packages feed

Agda 2.4.0.1 → 2.4.0.2

raw patch · 158 files changed

+1735/−1071 lines, 158 filesdep ~Agdadep ~basedep ~equivalence

Dependency ranges changed: Agda, base, equivalence

Files

Agda.cabal view
@@ -1,10 +1,10 @@ name:            Agda-version:         2.4.0.1+version:         2.4.0.2 cabal-version:   >= 1.8 build-type:      Custom license:         OtherLicense license-file:    LICENSE-author:          Ulf Norell, Nils Anders Danielsson, Andreas Abel, Makoto Takeyama, Catarina Coquand, with contributions by Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, James Chapman, Dominique Devriese, Peter Divanski, Fredrik Nordvall Forsberg, Olle Fredriksson, Daniel Gustafsson, Alan Jeffrey, Fredrik Lindblad, Guilhem Moulin, Nicolas Pouillard, Andrés Sicard-Ramírez and many more.+author:          Ulf Norell, Andreas Abel, Nils Anders Danielsson, Makoto Takeyama, Catarina Coquand, with contributions by Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, James Chapman, Jesper Cockx, Dominique Devriese, Peter Divanski, Fredrik Nordvall Forsberg, Olle Fredriksson, Daniel Gustafsson, Patrik Jansson, Alan Jeffrey, Wolfram Kahl, Fredrik Lindblad, Francesco Mazzoli, Stefan Monnier, Darin Morrison, Guilhem Moulin, Nicolas Pouillard, Andrés Sicard-Ramírez, Andrea Vezzosi and many more. maintainer:      Ulf Norell <ulfn@chalmers.se> homepage:        http://wiki.portal.chalmers.se/agda/ bug-reports:     http://code.google.com/p/agda/issues/list@@ -35,7 +35,7 @@ tested-with:        GHC == 7.2.2                     GHC == 7.4.2                     GHC == 7.6.3-                    GHC == 7.8.2+                    GHC == 7.8.3 extra-source-files: src/full/Agda/undefined.h                     README                     CHANGELOG@@ -56,7 +56,7 @@   type:     git   location: https://github.com/agda/agda.git   branch:   maint-2.4.0-  tag:      2.4.0.1+  tag:      2.4.0.2  flag epic   default: False@@ -101,7 +101,7 @@                     deepseq == 1.3.*,                     strict >= 0.3.2 && < 0.4,                     STMonadTrans >= 0.3.2 && < 0.4,-                    equivalence >= 0.2.3  && < 0.3,+                    equivalence >= 0.2.4  && < 0.3,                     boxes >= 0.1.3 && < 0.2,                     text >= 0.11 && < 1.2 @@ -112,8 +112,9 @@       build-depends:  time == 1.4.*,                       directory == 1.2.* -  build-tools:      happy >= 1.15 && < 2,-                    alex >= 2.3.1 && < 3.2+  build-tools:      happy >= 1.19.3 && < 2,+                    alex >= 3.1.0 && < 3.2+   -- LANGUAGE extension CPP is needed for cabal haddock (as of now, May 2014).   -- However, each file should define {-# LANGUAGE CPP #-}, for the sake   -- of ghci and make tags.@@ -151,10 +152,6 @@                     Agda.Compiler.MAlonzo.Misc                     Agda.Compiler.MAlonzo.Pretty                     Agda.Compiler.MAlonzo.Primitives-                    Agda.Packaging.Config-                    Agda.Packaging.Database-                    Agda.Packaging.Monad-                    Agda.Packaging.Types                     Agda.Interaction.CommandLine.CommandLine                     Agda.Interaction.EmacsCommand                     Agda.Interaction.Exceptions@@ -225,7 +222,7 @@                     Agda.Termination.TermCheck                     Agda.Termination.Termination                     Agda.Tests-                    Agda.TypeChecker+                    Agda.TheTypeChecker                     Agda.TypeChecking.Abstract                     Agda.TypeChecking.CheckInternal                     Agda.TypeChecking.CompiledClause@@ -341,6 +338,7 @@                     Agda.Utils.Maybe                     Agda.Utils.Maybe.Strict                     Agda.Utils.Monad+                    Agda.Utils.Null                     Agda.Utils.PartialOrd                     Agda.Utils.Permutation                     Agda.Utils.Pointer@@ -384,13 +382,6 @@                     -fwarn-overlapping-patterns                     -fwarn-unrecognised-pragmas                     -fwarn-warnings-deprecations-  -- The Cabal-generated module Paths_Agda triggers a warning under-  -- GHC 7.2.1/7.2.2 (at least when certain versions of Cabal are-  -- used).-  -- Issue 1103: Termination.SparseMatrix triggers a warning under GHC 7.0.4.-  -- -Werror is for developers only, who are assumed to use a recent GHC.-  -- if impl(ghc > 7.2.2)-  --   ghc-options:    -Werror   if impl(ghc >= 6.12)     ghc-options:    -fwarn-dodgy-exports                     -fwarn-wrong-do-bind@@ -411,7 +402,7 @@ executable agda   hs-source-dirs: src/main   main-is:        Main.hs-  build-depends:  Agda == 2.4.0.1,+  build-depends:  Agda == 2.4.0.2,                   -- Nothing is used from the following package, except                   -- for the prelude.                   base >= 3 && < 6
CHANGELOG view
@@ -1,4 +1,77 @@ ------------------------------------------------------------------------+-- Release notes for Agda 2 version 2.4.0.2+------------------------------------------------------------------------++Important changes since 2.4.0.1:++* The Agda input mode now supports alphabetical super and subscripts,+  in addition to the numerical ones that were already present.+  [Issue 1240]++* New feature: Interactively split result.++  Make case (C-c C-c) with no variables given tries to split on the+  result to introduce projection patterns.  The hole needs to be of+  record type, of course.++    test : {A B : Set} (a : A) (b : B) → A × B+    test a b = ?++  Result-splitting ? will produce the new clauses:++    proj₁ (test a b) = ?+    proj₂ (test a b) = ?++  If hole is of function type ending in a record type, the necessary+  pattern variables will be introduced before the split.  Thus, the+  same result can be obtained by starting from:++    test : {A B : Set} (a : A) (b : B) → A × B+    test = ?++* The so far undocumented ETA pragma now throws an error if applied to+  definitions that are not records.++  ETA can be used to force eta-equality at recursive record types,+  for which eta is not enabled automatically by Agda.+  Here is such an example:++    mutual+      data Colist (A : Set) : Set where+        [] : Colist A+        _∷_ : A → ∞Colist A → Colist A++      record ∞Colist (A : Set) : Set where+        coinductive+        constructor delay+        field       force : Colist A++    open ∞Colist++    {-# ETA ∞Colist #-}++    test : {A : Set} (x : ∞Colist A) → x ≡ delay (force x)+    test x = refl++  Note:  Unsafe use of ETA can make Agda loop, e.g. by triggering+  infinite eta expansion!++* Bugs fixed (see https://code.google.com/p/agda/issues):+  1203+  1205+  1209+  1213+  1214+  1216+  1225+  1226+  1231+  1233+  1239+  1241+  1243++------------------------------------------------------------------------ -- Release notes for Agda 2 version 2.4.0.1 ------------------------------------------------------------------------ @@ -118,7 +191,7 @@ ========  * 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:
LICENSE view
@@ -1,6 +1,11 @@-Copyright (c) 2005-2013 Ulf Norell, Nils Anders Danielsson, Catarina-Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, Marcin-Benke, Darin Morrison.+Copyright (c) 2005-2014 Ulf Norell, Andreas Abel, Nils Anders+Danielsson, Andrés Sicard-Ramírez, Dominique Devriese, Péter+Divianszki, Francesco Mazzoli, Stevan Andjelkovic, Daniel Gustafsson,+Alan Jeffrey, Makoto Takeyama, Andrea Vezzosi, Nicolas Pouillard,+James Chapman, Jean-Philippe Bernardy, Fredrik Lindblad, Nobuo+Yamashita, Fredrik Nordvall Forsberg, Patrik Jansson, Guilhem Moulin,+Stefan Monnier, Marcin Benke, Olle Fredriksson, Darin Morrison, Jesper+Cockx, Wolfram Kahl, Catarina Coquand  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the
dist/build/Agda/Syntax/Parser/Lexer.hs view
@@ -241,6 +241,7 @@ alex_action_98 =  identifier  {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-} {-# LINE 1 "<command-line>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- -----------------------------------------------------------------------------@@ -258,6 +259,7 @@   +-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex. #if __GLASGOW_HASKELL__ > 706 #define GTE(n,m) (tagToEnum# (n >=# m)) #define EQ(n,m) (tagToEnum# (n ==# m))@@ -265,11 +267,11 @@ #define GTE(n,m) (n >=# m) #define EQ(n,m) (n ==# m) #endif-{-# LINE 50 "templates/GenericTemplate.hs" #-}+{-# LINE 51 "templates/GenericTemplate.hs" #-}   data AlexAddr = AlexA# Addr#-+-- Do not remove this comment. Required to fix CPP parsing when using GCC and a clang-compiled alex. #if __GLASGOW_HASKELL__ < 503 uncheckedShiftL# = shiftL# #endif@@ -307,6 +309,7 @@ #else   indexInt32OffAddr# arr off #endif+
dist/build/Agda/Syntax/Parser/Parser.hs view
@@ -1,8 +1,5 @@ {-# OPTIONS_GHC -w #-} {-# OPTIONS -fglasgow-exts -cpp #-}-{-# OPTIONS_GHC -fno-warn-incomplete-patterns-                -fno-warn-deprecated-flags #-}-{-# LANGUAGE BangPatterns, PatternGuards #-} {-| The parser is generated by Happy (<http://www.haskell.org/happy>).  -  - Ideally, ranges should be as precise as possible, to get messages that@@ -24,7 +21,9 @@     ) where  import Control.Monad+ import Data.Char+import Data.Functor import Data.List import Data.Maybe import qualified Data.Traversable as T@@ -4149,7 +4148,7 @@ happyReduction_330 happy_x_1 	 =  case happyOutTok happy_x_1 of { (TokId happy_var_1) ->  	happyIn103-		 (Ranged (getRange $ fst happy_var_1) (snd happy_var_1)+		 (Ranged (getRange $ fst happy_var_1) (stringToRawName $ snd happy_var_1) 	)}  happyReduce_331 = happySpecReduce_1  98# happyReduction_331@@ -4184,12 +4183,12 @@     ; dir = happy_var_5     ; r   = getRange (m, es, dir)     ; mr  = getRange m-    ; unique = hashString $ show $ fmap (const (Nothing :: Maybe ())) r+    ; unique = hashString $ show $ (Nothing :: Maybe ()) <$ r          -- turn range into unique id, but delete file path          -- which is absolute and messes up suite of failing tests          -- (different hashs on different installations)          -- TODO: Don't use (insecure) hashes in this way.-    ; fresh = Name mr [ Id $ ".#" ++ show m ++ "-" ++ show unique ]+    ; fresh = Name mr [ Id $ stringToRawName $ ".#" ++ show m ++ "-" ++ show unique ]     ; impStm asR = Import mr m (Just (AsName fresh asR)) DontOpen defaultImportDir     ; appStm m' es =         let r = getRange (m, es) in@@ -4203,7 +4202,7 @@     ; parseAsClause = case last2Args of       { [ Ident (QName (Name asR [Id x]))         , Ident (QName m')-        ] | x == "as" -> Just (asR, m')+        ] | rawNameToString x == "as" -> Just (asR, m')       ; _ -> Nothing       }     } in@@ -5098,7 +5097,9 @@     return $ Name (getRange i) xs     where 	isValidId Hole   = return ()-	isValidId (Id x) = case parse defaultParseFlags [0] (lexer return) x of+	isValidId (Id y) = do+          let x = rawNameToString y+          case parse defaultParseFlags [0] (lexer return) x of 	    ParseOk _ (TokId _) -> return () 	    _			-> fail $ "in the name " ++ s ++ ", the part " ++ x ++ " is not valid" @@ -5272,10 +5273,10 @@     Equal _ a b -> Just (stripSingletonRawApp a, stripSingletonRawApp b)     _           -> Nothing -maybeNamed :: Expr -> Named RString Expr+maybeNamed :: Expr -> Named_ Expr maybeNamed e =   case isEqual e of-    Just (Ident (QName x), b) -> named (Ranged (getRange x) (show x)) b+    Just (Ident (QName x), b) -> named (Ranged (getRange x) (nameToRawName x)) b     _                         -> unnamed e  patternSynArgs :: [Either Hiding LamBinding] -> Parser [Arg Name]@@ -5320,6 +5321,7 @@   ] {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-} {-# LINE 1 "<command-line>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp
src/data/emacs-mode/agda-input.el view
@@ -850,6 +850,72 @@   ("Mfy" . ("𝔶"))   ("Mfz" . ("𝔷")) +  ;; (Sub / Super) scripts++  ("_a" . ("ₐ"))+  ("_e" . ("ₑ"))+  ("_h" . ("ₕ"))+  ("_i" . ("ᵢ"))+  ("_j" . ("ⱼ"))+  ("_k" . ("ₖ"))+  ("_l" . ("ₗ"))+  ("_m" . ("ₘ"))+  ("_n" . ("ₙ"))+  ("_o" . ("ₒ"))+  ("_p" . ("ₚ"))+  ("_r" . ("ᵣ"))+  ("_s" . ("ₛ"))+  ("_t" . ("ₜ"))+  ("_u" . ("ᵤ"))+  ("_v" . ("ᵥ"))+  ("_x" . ("ₓ"))++  ("^a" . ("ᵃ"))+  ("^b" . ("ᵇ"))+  ("^c" . ("ᶜ"))+  ("^d" . ("ᵈ"))+  ("^e" . ("ᵉ"))+  ("^f" . ("ᶠ"))+  ("^g" . ("ᵍ"))+  ("^h" . ("ʰ"))+  ("^i" . ("ⁱ"))+  ("^j" . ("ʲ"))+  ("^k" . ("ᵏ"))+  ("^l" . ("ˡ"))+  ("^m" . ("ᵐ"))+  ("^n" . ("ⁿ"))+  ("^o" . ("ᵒ"))+  ("^p" . ("ᵖ"))+  ("^r" . ("ʳ"))+  ("^s" . ("ˢ"))+  ("^t" . ("ᵗ"))+  ("^u" . ("ᵘ"))+  ("^v" . ("ᵛ"))+  ("^w" . ("ʷ"))+  ("^x" . ("ˣ"))+  ("^y" . ("ʸ"))+  ("^z" . ("ᶻ"))++  ("^A" . ("ᴬ"))+  ("^B" . ("ᴮ"))+  ("^D" . ("ᴰ"))+  ("^E" . ("ᴱ"))+  ("^G" . ("ᴳ"))+  ("^H" . ("ᴴ"))+  ("^I" . ("ᴵ"))+  ("^J" . ("ᴶ"))+  ("^K" . ("ᴷ"))+  ("^L" . ("ᴸ"))+  ("^M" . ("ᴹ"))+  ("^N" . ("ᴺ"))+  ("^O" . ("ᴼ"))+  ("^P" . ("ᴾ"))+  ("^R" . ("ᴿ"))+  ("^T" . ("ᵀ"))+  ("^U" . ("ᵁ"))+  ("^V" . ("ⱽ"))+  ("^W" . ("ᵂ"))+   ;; Some ISO8859-1 characters.    (" "         . (" "))
src/data/emacs-mode/agda2-highlight.el view
@@ -117,7 +117,7 @@             (agda2-highlight-dotted-face)             (agda2-highlight-error-face              :foreground "red"-             :underline)+             :underline t)             (agda2-highlight-unsolved-meta-face              :foreground "black"              :background "yellow")
src/data/emacs-mode/agda2-mode.el view
@@ -10,7 +10,7 @@  ;;; Code: -(defvar agda2-version "2.4.0.1"+(defvar agda2-version "2.4.0.2"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.")
src/full/Agda/Auto/Auto.hs view
@@ -46,6 +46,7 @@ #include "../undefined.h" import Agda.Utils.Impossible +insertAbsurdPattern :: String -> String insertAbsurdPattern [] = [] insertAbsurdPattern s@(_:_) | take (length abspatvarname) s == abspatvarname = "()" ++ drop (length abspatvarname) s insertAbsurdPattern (c:s) = c : insertAbsurdPattern s@@ -58,6 +59,25 @@  dispmsg msg = return (Left [], Just msg) +-- | Entry point for Auto tactic (Agsy).+--+--     @auto ii rng s = return (res, mmsg)@+--+--   If @mmsg = Just msg@, the message @msg@ produced by Agsy should+--   be displayed to the user.+--+--   The result @res@ of the Auto tactic can be one of the following three:+--+--   1. @Left [(ii,s)]@+--      A list of solutions @s@ for interaction ids @ii@.+--      In particular, @Left []@ means Agsy found no solution.+--+--   2. @Right (Left cs)@+--      A list of clauses (the user allowed case-split).+--+--   3. @Right (Right s)@+--      A refinement for the interaction id @ii@ in which Auto was invoked.+ auto :: InteractionId -> Range -> String -> TCM (Either [(InteractionId, String)] (Either [String] String), Maybe String) auto ii rng argstr = liftTCM $ do          let (hints, timeout, pick, mode, hintmode) = parseargs argstr@@ -282,8 +302,7 @@                    (ids, pats) <- constructPats cmap mi clause-                 let pids = concat $ map (\(_, x) -> " " ++ case x of {Id s -> s; NoId -> "noid"}) ids-                     ctx = map (\((hid, id), t) -> HI hid (id, t)) (zip ids mylocalVars)+                 let ctx = map (\((hid, id), t) -> HI hid (id, t)) (zip ids mylocalVars)                  ticks <- liftIO $ newIORef 0                  let [rectyp'] = mymrectyp                  defdfv <- getdfv mi def
src/full/Agda/Auto/CaseSplit.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE Rank2Types, ScopedTypeVariables, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+ module Agda.Auto.CaseSplit where  import Data.IORef@@ -14,6 +17,7 @@ #include "../undefined.h" import Agda.Utils.Impossible +abspatvarname :: String abspatvarname = "\0absurdPattern"  costCaseSplitVeryHigh = 10000@@ -134,7 +138,7 @@            case findperm (map snd (drophid ctx)) of             Just perm ->              let HI scrhid(_, scrt) = ctx !! scrut-                 ctx1 = take scrut ctx ++ (HI scrhid (Id abspatvarname, scrt)) : drop (scrut + 1) ctx+                 ctx1 = take scrut ctx ++ (HI scrhid (stringToMyId abspatvarname, scrt)) : drop (scrut + 1) ctx                  (ctx', _, pats') = applyperm perm ctx1 tt ({-map (replacep scrut 1 CSAbsurd __IMPOSSIBLE__) -}pats)              in [(ctx', pats', Nothing)]             Nothing -> __IMPOSSIBLE__ -- no permutation found
src/full/Agda/Auto/NarrowingSearch.hs view
@@ -1,7 +1,11 @@-{-# LANGUAGE UndecidableInstances, Rank2Types,-             ExistentialQuantification, MultiParamTypeClasses,-             FunctionalDependencies, FlexibleInstances,-             ScopedTypeVariables, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}  module Agda.Auto.NarrowingSearch where
src/full/Agda/Auto/SearchControl.hs view
@@ -1,5 +1,8 @@-{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses,-             TypeSynonymInstances, FlexibleInstances, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}  module Agda.Auto.SearchControl where
src/full/Agda/Auto/Syntax.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE ExistentialQuantification, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ExistentialQuantification #-}  module Agda.Auto.Syntax where @@ -71,6 +72,9 @@  data MId = Id String          | NoId++stringToMyId :: String -> MId+stringToMyId = Id  -- | Abstraction with maybe a name. --
src/full/Agda/Auto/Typecheck.hs view
@@ -1,5 +1,7 @@-{-# LANGUAGE ExistentialQuantification, FlexibleContexts,-             ScopedTypeVariables, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Agda.Auto.Typecheck where
src/full/Agda/Compiler/Epic/AuxAST.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ -- | Intermediate abstract syntax tree used in the compiler. Pretty close to --   Epic syntax. module Agda.Compiler.Epic.AuxAST where
src/full/Agda/Compiler/Epic/Compiler.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ -- | Epic compiler backend. module Agda.Compiler.Epic.Compiler(compilerMain) where
src/full/Agda/Compiler/Epic/Erasure.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ -- | Some arguments to functions (types in particular) will not be used in the --   body. Wouldn't it be useful if these wasn't passed around at all? --   Fear not, we here perform some analysis and try to remove as many of these
src/full/Agda/Compiler/Epic/ForceConstrs.hs view
@@ -1,5 +1,6 @@ -- | Remove forced arguments from constructors. {-# LANGUAGE CPP #-}+ module Agda.Compiler.Epic.ForceConstrs where  import Control.Applicative
src/full/Agda/Compiler/Epic/Forcing.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+ module Agda.Compiler.Epic.Forcing where  import Control.Applicative
src/full/Agda/Compiler/Epic/Injection.hs view
@@ -1,4 +1,10 @@-{-# LANGUAGE CPP, TypeOperators, PatternGuards, FlexibleInstances, TypeSynonymInstances, OverlappingInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE OverlappingInstances #-}+ module Agda.Compiler.Epic.Injection where  import Control.Monad.State@@ -18,11 +24,12 @@ import Agda.TypeChecking.CompiledClause import Agda.TypeChecking.Monad import Agda.TypeChecking.Monad.Builtin-import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Pretty hiding (empty) import Agda.TypeChecking.Reduce import Agda.TypeChecking.Substitute import Agda.Utils.List import Agda.Utils.Monad+import Agda.Utils.Null import qualified Agda.Utils.HashMap as HM  import Agda.Compiler.Epic.CompileState@@ -45,7 +52,7 @@         Just inj@(InjectiveFun nvar arity) -> case theDef def of             f@(Function{})   -> do                 modifyEI $ \s -> s { injectiveFuns = M.insert q inj (injectiveFuns s) }-                let ns = replicate arity (defaultArg "")+                let ns = replicate arity (defaultArg empty)                 return $ (,) q $ def { theDef = f { funCompiled = Just $ Done ns $                                                       var $ arity - nvar - 1 } }             _                -> __IMPOSSIBLE__
src/full/Agda/Compiler/Epic/NatDetection.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ -- | Detect if a datatype could be represented as a primitive integer. --   If it has one constructor with no arguments and one with a recursive --   argument this is true. This is done using IrrFilters which filter out
src/full/Agda/Compiler/Epic/Smashing.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ -- | Smash functions which return something that can be inferred --   (something of a type with only one element)
src/full/Agda/Compiler/Epic/Static.hs view
@@ -1,7 +1,9 @@ -- | Find the places where the builtin static is used and do some normalisation --   there. -{-# LANGUAGE CPP, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.Compiler.Epic.Static where
src/full/Agda/Compiler/JS/Compiler.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, NamedFieldPuns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE NamedFieldPuns #-}  module Agda.Compiler.JS.Compiler where
src/full/Agda/Compiler/MAlonzo/Compiler.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}  module Agda.Compiler.MAlonzo.Compiler where
src/full/Agda/Compiler/MAlonzo/Pretty.hs view
@@ -2,8 +2,10 @@ -- Pretty-printing of Haskell modules ------------------------------------------------------------------------ -{-# LANGUAGE FlexibleContexts, FlexibleInstances,-             MultiParamTypeClasses, TemplateHaskell #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}  module Agda.Compiler.MAlonzo.Pretty where
src/full/Agda/Compiler/MAlonzo/Primitives.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.Compiler.MAlonzo.Primitives where  import Control.Monad.Reader
src/full/Agda/ImpossibleTest.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.ImpossibleTest where  #include "undefined.h"
src/full/Agda/Interaction/BasicOps.hs view
@@ -1,7 +1,9 @@-{-# LANGUAGE CPP, TupleSections,-             MultiParamTypeClasses, FlexibleInstances,-             UndecidableInstances, DeriveFunctor-  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE UndecidableInstances #-}  module Agda.Interaction.BasicOps where @@ -11,6 +13,7 @@ import Control.Monad.Reader import Control.Monad.State import Control.Monad.Identity+ import qualified Data.Map as Map import Data.List import Data.Maybe@@ -32,7 +35,7 @@ import Agda.Syntax.Fixity(Precedence(..)) import Agda.Syntax.Parser -import Agda.TypeChecker+import Agda.TheTypeChecker import Agda.TypeChecking.Conversion import Agda.TypeChecking.Monad as M hiding (MetaInfo) import Agda.TypeChecking.MetaVars@@ -47,6 +50,7 @@ import Agda.TypeChecking.Free (freeIn) import qualified Agda.TypeChecking.Pretty as TP +import Agda.Utils.Functor import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Monad@@ -509,6 +513,7 @@                 | otherwise    -> subst __IMPOSSIBLE__ (unEl b)       _ -> v  -- todo: handle if goal type is a Pi +    -- renameVars = onNames (stringToArgName <.> renameVar . argNameToString)     renameVars = onNames renameVar      hiding args (El s v) = El s $ hidingTm args v@@ -517,9 +522,11 @@     hidingTm args (I.Pi a b) = I.Pi a (hiding args <$> b)     hidingTm _ a = a +    -- onNames :: Applicative m => (ArgName -> m ArgName) -> Type -> m Type     onNames :: Applicative m => (String -> m String) -> Type -> m Type     onNames f (El s v) = El s <$> onNamesTm f v +    -- onNamesTel :: Applicative f => (ArgName -> f ArgName) -> I.Telescope -> f I.Telescope     onNamesTel :: Applicative f => (String -> f String) -> I.Telescope -> f I.Telescope     onNamesTel f I.EmptyTel = pure I.EmptyTel     onNamesTel f (I.ExtendTel a b) = I.ExtendTel <$> traverse (onNames f) a <*> onNamesAbs f onNamesTel b@@ -538,8 +545,9 @@       I.Shared{}   -> pure v     onNamesElims f = traverse $ traverse $ onNamesTm f     onNamesArgs f  = traverse $ traverse $ onNamesTm f-    onNamesAbs f nd (Abs   s x) = Abs   <$> f s <*> nd f x-    onNamesAbs f nd (NoAbs s x) = NoAbs <$> f s <*> nd f x+    onNamesAbs f   = onNamesAbs' f (stringToArgName <.> f . argNameToString)+    onNamesAbs' f f' nd (Abs   s x) = Abs   <$> f' s <*> nd f x+    onNamesAbs' f f' nd (NoAbs s x) = NoAbs <$> f' s <*> nd f x      unW "w" = return ".w"     unW s   = return s@@ -553,7 +561,7 @@       put args       return $ case arg of         Arg _ (Named _ (A.Var x)) -> show x-        Arg _ (Named (Just x) _)  -> rangedThing x+        Arg _ (Named (Just x) _)  -> argNameToString $ rangedThing x         _                         -> "w"
src/full/Agda/Interaction/CommandLine/CommandLine.hs view
@@ -5,6 +5,7 @@ import Control.Monad.Error import Control.Monad.Reader import Control.Applicative+ import Data.List as List import Data.Maybe @@ -13,6 +14,7 @@  import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Common+import qualified Agda.Syntax.Internal as I import Agda.Syntax.Parser import Agda.Syntax.Position import Agda.Syntax.Scope.Base@@ -21,7 +23,7 @@  import Text.PrettyPrint -import Agda.TypeChecker+import Agda.TheTypeChecker import Agda.TypeChecking.Constraints import Agda.TypeChecking.Monad import Agda.TypeChecking.Reduce@@ -263,7 +265,7 @@ 		    ["normal"] -> normalise $ raise n t 		    _	       -> return $ raise n t 	    d <- prettyTCM t-	    liftIO $ print $ text x <+> text ":" <+> d+	    liftIO $ print $ text (I.argNameToString x) <+> text ":" <+> d showContext _ = liftIO $ putStrLn ":Context meta"  -- | The logo that prints when Agda is started in interactive mode.
src/full/Agda/Interaction/EmacsTop.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE CPP, ScopedTypeVariables, FlexibleInstances #-}+-- {-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+ module Agda.Interaction.EmacsTop     ( mimicGHCi     ) where
src/full/Agda/Interaction/Highlighting/Dot.hs view
@@ -1,4 +1,7 @@ {-# LANGUAGE CPP #-}++-- | Generate an import dependency graph for a given module.+ module Agda.Interaction.Highlighting.Dot where  import Control.Applicative@@ -19,10 +22,17 @@ #include "../../undefined.h" import Agda.Utils.Impossible +-- | Internal module identifiers for construction of dependency graph.+type ModuleId = String+ data DotState = DotState-  { dsModules    :: Map ModuleName String-  , dsNameSupply :: [String]-  , dsConnection :: Set (String, String)+  { dsModules    :: Map ModuleName ModuleId+    -- ^ Records already processed modules+    --   and maps them to an internal identifier.+  , dsNameSupply :: [ModuleId]+    -- ^ Supply of internal identifiers.+  , dsConnection :: Set (ModuleId, ModuleId)+    -- ^ Edges of dependency graph.   }  initialDotState :: DotState@@ -34,7 +44,10 @@  type DotM = StateT DotState TCM -addModule :: ModuleName -> DotM (String, Bool)+-- | Translate a 'ModuleName' to an internal 'ModuleId'.+--   Returns @True@ if the 'ModuleName' is new, i.e., has not been+--   encountered before and is thus added to the map of processed modules.+addModule :: ModuleName -> DotM (ModuleId, Bool) addModule m = do     s <- get     case M.lookup m (dsModules s) of@@ -47,29 +60,35 @@               }             return (newName, True) --addConnection :: String -> String -> DotM ()+-- | Add an arc from importer to imported.+addConnection :: ModuleId -> ModuleId -> DotM () addConnection m1 m2 = modify $ \s -> s {dsConnection = S.insert (m1,m2) (dsConnection s)} -dottify :: Interface -> DotM String+-- | Recursively build import graph, starting from given 'Interface'.+--   Modifies the state in 'DotM' and returns the 'ModuleId' of the 'Interface'.+dottify :: Interface -> DotM ModuleId dottify inter = do     let curModule = iModuleName inter     (name, continue) <- addModule curModule-    importsifs <- lift $ map miInterface . catMaybes <$> mapM (getVisitedModule . toTopLevelModuleName . fst) (iImportedModules inter)+    -- If we have not visited this interface yet,+    -- process its imports recursively and+    -- add them as connections to the graph.     when continue $ do+        importsifs <- lift $ map miInterface . catMaybes <$>+          mapM (getVisitedModule . toTopLevelModuleName . fst) (iImportedModules inter)         imports    <- mapM dottify importsifs         mapM_ (addConnection name) imports     return name -+-- | Generate a .dot file for the import graph starting with the+--   given 'Interface' and write it to the file specified by the+--   command line option. generateDot :: Interface -> TCM () generateDot inter = do     (top, state) <- flip runStateT initialDotState $ do         dottify inter-    mfile <- optDependencyGraph <$> commandLineOptions-    case mfile of-        Nothing -> __IMPOSSIBLE__-        Just fp -> liftIO $ writeFile fp $ mkDot state+    fp <- fromMaybe __IMPOSSIBLE__ . optDependencyGraph <$> commandLineOptions+    liftIO $ writeFile fp $ mkDot state   where     mkDot :: DotState -> String     mkDot st = unlines $
src/full/Agda/Interaction/Highlighting/Generate.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, FlexibleContexts, RelaxedPolyRec #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE RelaxedPolyRec #-}  -- | Generates data used for precise syntax highlighting. @@ -251,7 +253,7 @@     getVarAndField (A.Rec _ fs) = mconcat $ map (field [] . fst) fs     getVarAndField _            = mempty -    -- Ulf, 2014-04-09: It would be nicer to have it on Named RString a, but+    -- Ulf, 2014-04-09: It would be nicer to have it on Named_ a, but     -- you can't have polymorphic functions in universeBi.     getNamedArg :: SC.RString -> File     getNamedArg x = singleton (rToR $ P.getRange x) mempty{ aspect = Just $ Name (Just Argument) False }
src/full/Agda/Interaction/Highlighting/HTML.hs view
@@ -11,28 +11,34 @@ import Control.Monad import Control.Monad.Trans import Control.Monad.State.Class-import Control.Arrow ((***))-import System.FilePath-import System.Directory-import Text.XHtml.Strict+ import Data.Function import Data.Monoid import Data.Maybe import qualified Data.Map  as Map import qualified Data.List as List +import System.FilePath+import System.Directory++import Text.XHtml.Strict+ import Paths_Agda  import Agda.Interaction.Highlighting.Precise-import Agda.TypeChecking.Monad (TCM)-import qualified Agda.TypeChecking.Monad as TCM+import Agda.Interaction.Options+ import qualified Agda.Syntax.Abstract as A import qualified Agda.Syntax.Concrete as C import Agda.Syntax.Common-import Agda.Interaction.Options++import Agda.TypeChecking.Monad (TCM)+import qualified Agda.TypeChecking.Monad as TCM+ import Agda.Utils.FileName (filePath) import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.Pretty+import Agda.Utils.Tuple  #include "../../undefined.h" import Agda.Utils.Impossible@@ -42,14 +48,14 @@ defaultCSSFile :: FilePath defaultCSSFile = "Agda.css" --- | Generates HTML files from all the sources which the given module--- depends on (including the module itself).+-- | Generates HTML files from all the sources which have been+--   visited during the type checking phase. ----- This function should only be called after type checking has--- completed successfully.+--   This function should only be called after type checking has+--   completed successfully. -generateHTML :: A.ModuleName -> TCM ()-generateHTML mod = do+generateHTML :: TCM ()+generateHTML = do       options <- TCM.commandLineOptions        -- There is a default directory given by 'defaultHTMLDir'@@ -71,7 +77,7 @@       -- Pull highlighting info from the state and generate all the       -- web pages.       mapM_ (\(m, h) -> generatePage dir m h) =<<-        map (id *** TCM.iHighlighting . TCM.miInterface) .+        map (mapSnd $ TCM.iHighlighting . TCM.miInterface) .           Map.toList <$> TCM.getVisitedModules  -- | Converts module names to the corresponding HTML file names.
src/full/Agda/Interaction/Highlighting/LaTeX.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, ViewPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ViewPatterns #-}  -- | Function for generating highlighted and aligned LaTeX from literate -- Agda source.@@ -27,13 +28,16 @@ import Paths_Agda  import Agda.Syntax.Common-import qualified Agda.Syntax.Abstract as A+import Agda.Syntax.Concrete (TopLevelModuleName, moduleNameParts)+import qualified Agda.Interaction.FindFile as Find import Agda.Interaction.Highlighting.Precise import Agda.TypeChecking.Monad (TCM) import qualified Agda.TypeChecking.Monad as TCM import Agda.Interaction.Options import Agda.Compiler.CallCompiler import qualified Agda.Utils.IO.UTF8 as UTF8+import Agda.Utils.FileName (filePath)+import Agda.Utils.Pretty (pretty, render)  #include "../../undefined.h" import Agda.Utils.Impossible@@ -473,7 +477,7 @@ defaultStyFile = "agda.sty"  -- | The only exported function. It's (only) called in @Main.hs@.-generateLaTeX :: A.ModuleName -> HighlightingInfo -> TCM ()+generateLaTeX :: TopLevelModuleName -> HighlightingInfo -> TCM () generateLaTeX mod hi = do    options <- TCM.commandLineOptions@@ -501,20 +505,18 @@       styFile <- getDataFileName defaultStyFile       liftIO $ copyFile styFile (dir </> defaultStyFile) +  let outPath = modToFile mod+  inAbsPath <- liftM filePath (Find.findFile mod)+   liftIO $ do-    let filePath = modToFile mod-    source <- UTF8.readTextFile (filePath <.> "lagda")+    source <- UTF8.readTextFile inAbsPath     latex <- E.encodeUtf8 `fmap` toLaTeX source hi-    createDirectoryIfMissing True $ dir </> takeDirectory filePath-    BS.writeFile (dir </> filePath <.> "tex") latex+    createDirectoryIfMissing True $ dir </> takeDirectory outPath+    BS.writeFile (dir </> outPath) latex    where-  modToFile :: A.ModuleName -> FilePath-  modToFile mod = go $ show mod-    where-    go []         = []-    go ('.' : cs) = pathSeparator : go cs-    go (c   : cs) = c             : go cs+    modToFile :: TopLevelModuleName -> FilePath+    modToFile m = List.intercalate [pathSeparator] (moduleNameParts m) <.> "tex"  -- | Transforms the source code into LaTeX. toLaTeX :: String -> HighlightingInfo -> IO Text
src/full/Agda/Interaction/Highlighting/Vim.hs view
@@ -3,13 +3,15 @@ module Agda.Interaction.Highlighting.Vim where  import Control.Monad.Trans-import Data.Function ( on )-import System.FilePath +import Data.Function ( on ) import qualified Data.List as List import qualified Data.Map as Map +import System.FilePath+ import Agda.Syntax.Scope.Base+import Agda.Syntax.Common import Agda.Syntax.Concrete.Name as CName  import Agda.TypeChecking.Monad@@ -17,9 +19,6 @@ import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.Tuple --- defined in Data.Function--- on f g x y = f (g x) (g y)- vimFile :: FilePath -> FilePath vimFile file =     case splitFileName file of@@ -80,7 +79,7 @@  	parts (NoName _ _) = [] 	parts (Name _ [_]) = []-	parts (Name _ ps)  = [ x | Id x <- ps ]+	parts (Name _ ps)  = [ rawNameToString x | Id x <- ps ]  generateVimFile :: FilePath -> TCM () generateVimFile file = do
src/full/Agda/Interaction/Imports.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, TupleSections #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}+ {-| This module deals with finding imported modules and loading their     interface files. -}@@ -44,7 +46,7 @@ import Agda.TypeChecking.Monad.Benchmark (billTop, reimburseTop) import qualified Agda.TypeChecking.Monad.Benchmark as Bench -import Agda.TypeChecker+import Agda.TheTypeChecker  import Agda.Interaction.FindFile import Agda.Interaction.Options
src/full/Agda/Interaction/InteractionTop.hs view
@@ -1,8 +1,15 @@-{-# LANGUAGE CPP, TupleSections,-  ScopedTypeVariables, Rank2Types,-  MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances,-  GeneralizedNewtypeDeriving,-  DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+ {-# OPTIONS -fno-cse #-}  module Agda.Interaction.InteractionTop@@ -68,11 +75,12 @@ import qualified Agda.Auto.Auto as Auto  import Agda.Utils.FileName+import Agda.Utils.Hash import qualified Agda.Utils.HashMap as HMap+import Agda.Utils.Monad import Agda.Utils.Pretty-import Agda.Utils.Time-import Agda.Utils.Hash import Agda.Utils.String+import Agda.Utils.Time  #include "../undefined.h" import Agda.Utils.Impossible@@ -95,12 +103,14 @@     -- the file when it was last loaded.   , optionsOnReload :: CommandLineOptions     -- ^ Reset the options on each reload to these.-  , oldInteractionScopes :: Map InteractionId ScopeInfo+  , oldInteractionScopes :: OldInteractionScopes     -- ^ 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.   } +type OldInteractionScopes = Map InteractionId ScopeInfo+ -- | Initial auxiliary interaction state  initCommandState :: CommandState@@ -155,15 +165,22 @@   s { theInteractionPoints = f (theInteractionPoints s) }  --- | Operations for manipulating 'oldInteractionScopes'.+-- * Operations for manipulating 'oldInteractionScopes'. +-- | A Lens for 'oldInteractionScopes'.+modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()+modifyOldInteractionScopes f = modify $ \ s ->+  s { oldInteractionScopes = f $ oldInteractionScopes s }+ insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()-insertOldInteractionScope ii scope =-  modify $ \s -> s { oldInteractionScopes = Map.insert ii scope $ oldInteractionScopes s }+insertOldInteractionScope ii scope = do+  lift $ reportSLn "interaction.scope" 20 $ "inserting old interaction scope " ++ show ii+  modifyOldInteractionScopes $ Map.insert ii scope  removeOldInteractionScope :: InteractionId -> CommandM ()-removeOldInteractionScope ii =-  modify $ \s -> s { oldInteractionScopes = Map.delete ii $ oldInteractionScopes s }+removeOldInteractionScope ii = do+  lift $ reportSLn "interaction.scope" 20 $ "removing old interaction scope " ++ show ii+  modifyOldInteractionScopes $ Map.delete ii  getOldInteractionScope :: InteractionId -> CommandM ScopeInfo getOldInteractionScope ii = do@@ -580,12 +597,23 @@ interpret (Cmd_highlight ii rng s) = withCurrentFile $ do   scope <- getOldInteractionScope ii   removeOldInteractionScope ii-  lift (do-    e     <- concreteToAbstract scope =<< B.parseExpr rng s-    printHighlightingInfo =<< generateTokenInfoFromString rng s-    highlightExpr e)-  `catchError` \_ ->-    display_info $ Info_Error $ "Failed to parse expression in " ++ show ii+  handle $ do+    e <- try ("Highlighting failed to parse expression in " ++ show ii) $+           B.parseExpr rng s+    e <- try ("Highlighting failed to scope check expression in " ++ show ii) $+           concreteToAbstract scope e+    lift $ printHighlightingInfo =<< generateTokenInfoFromString rng s+    lift $ highlightExpr e+  where+    handle :: ErrorT String TCM () -> CommandM ()+    handle m = do+      res <- lift $ runErrorT m+      case res of+        Left s  -> display_info $ Info_Error s+        Right _ -> return ()+    try :: String -> TCM a -> ErrorT String TCM a+    try err m = ErrorT $ do+      (Right <$> m) `catchError` \ _ -> return (Left err)  interpret (Cmd_give   ii rng s) = give_gen ii rng s Give interpret (Cmd_refine ii rng s) = give_gen ii rng s Refine@@ -610,12 +638,27 @@   (if null s then Cmd_intro pmLambda else Cmd_refine) ii r s  interpret (Cmd_auto ii rng s) = do+  -- Andreas, 2014-07-05 Issue 1226:+  -- Save the state to have access to even those interaction ids+  -- that Auto solves (since Auto gives the solution right away).+  st <- lift $ get   (res, msg) <- lift $ Auto.auto ii rng s   case res of    Left xs -> do+    lift $ reportSLn "auto" 10 $ "Auto produced the following solutions " ++ show xs     forM_ xs $ \(ii, s) -> do-      modifyTheInteractionPoints $ filter (/= ii)+      -- Andreas, 2014-07-05 Issue 1226:+      -- For highlighting, Resp_GiveAction needs to access+      -- the @oldInteractionScope@s of the interaction points solved by Auto.+      -- We dig them out from the state before Auto was invoked.+      insertOldInteractionScope ii =<< lift (localState (put st >> getInteractionScope ii))+      -- Andreas, 2014-07-07: NOT TRUE:+      -- -- Andreas, 2014-07-05: The following should be obsolete,+      -- -- as Auto has removed the interaction points already:+      -- modifyTheInteractionPoints $ filter (/= ii)       putResponse $ Resp_GiveAction ii $ Give_String s+    -- Andreas, 2014-07-07: Remove the interaction points in one go.+    modifyTheInteractionPoints (\\ (map fst xs))     case msg of      Nothing -> interpret Cmd_metas      Just msg -> display_info $ Info_Auto msg@@ -796,6 +839,7 @@   -> GiveRefine   -> CommandM () give_gen ii rng s giveRefine = withCurrentFile $ do+  lift $ reportSLn "interaction.give" 20 $ "give_gen  " ++ s   let give_ref =         case giveRefine of           Give   -> B.give@@ -812,7 +856,7 @@     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+  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@@ -1047,15 +1091,16 @@   displayStatus   putResponse $ Resp_DisplayInfo info -takenNameStr :: TCM [String]-takenNameStr = do-  xss <- sequence [ List.map (fst . unDom) <$> getContext-                  , Map.keys <$> asks envLetBindings-                  , List.map qnameName . HMap.keys . sigDefinitions <$> getSignature-		  ]-  return $ concat [ parts $ nameConcrete x | x <- concat xss]-  where-    parts x = [ s | Id s <- nameParts x ]+-- UNUSED+-- takenNameStr :: TCM [String]+-- takenNameStr = do+--   xss <- sequence [ List.map (fst . unDom) <$> getContext+--                   , Map.keys <$> asks envLetBindings+--                   , List.map qnameName . HMap.keys . sigDefinitions <$> getSignature+-- 		  ]+--   return $ concat [ parts $ nameConcrete x | x <- concat xss]+--   where+--     parts x = [ s | Id s <- nameParts x ]  refreshStr :: [String] -> String -> ([String], String) refreshStr taken s = go nameModifiers where
src/full/Agda/Interaction/MakeCase.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, TupleSections #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE TupleSections #-}  module Agda.Interaction.MakeCase where @@ -21,7 +23,7 @@ import Agda.TypeChecking.Reduce import Agda.TypeChecking.Substitute import Agda.TypeChecking.Irrelevance-import Agda.TypeChecker+import Agda.TheTypeChecker  import Agda.Interaction.BasicOps @@ -111,24 +113,31 @@       , text "ps      =" <+> text (show ps)       ]     ]-  -- vars <- mapM (\s -> deBruijnIndex =<< parseExprIn hole rng s) $ words s-  vars <- parseVariables hole rng $ words s-  (casectxt,) <$> split f vars clause+  let vars = words s+  if null vars then do+    -- split result+    res <- splitResult f =<< fixTarget (clauseToSplitClause clause)+    case res of+      Nothing  -> typeError $ GenericError $ "Cannot split on result here"+      Just cov -> (casectxt,) <$> do mapM (makeAbstractClause f) $ splitClauses cov+  else do+    -- split on variables+    vars <- parseVariables hole rng vars+    (casectxt,) <$> split f vars clause   where   split :: QName -> [Nat] -> Clause -> TCM [A.Clause]   split f [] clause =     (:[]) <$> makeAbstractClause f (clauseToSplitClause clause)   split f (var : vars) clause = do-    z <- splitClauseWithAbs clause var+    z <- splitClauseWithAbsurd clause var     case z of       Left err          -> typeError $ SplitError err       Right (Left cl)   -> (:[]) <$> makeAbsurdClause f cl       Right (Right cov)         | null vars -> mapM (makeAbstractClause f) $ splitClauses cov         | otherwise -> concat <$> do-            mapM (\cl -> split f (mapMaybe (newVar cl) vars)-                                 (splitClauseToClause cl))-                 $ splitClauses cov+            forM (splitClauses cov) $ \ cl ->+              split f (mapMaybe (newVar cl) vars) $ splitClauseToClause cl     where     -- Note that the body of the created clause is the body of the     -- argument to split.@@ -144,8 +153,8 @@    -- Finds the new variable corresponding to an old one, if any.   newVar :: SplitClause -> Nat -> Maybe Nat-  newVar c x = case ignoreSharing $ applySubst (scSubst c) (Var x []) of-    Var x [] -> Just x+  newVar c x = case ignoreSharing $ applySubst (scSubst c) (var x) of+    Var y [] -> Just y     _        -> Nothing    -- NOTE: clauseToSplitClause moved to Coverage.hs
src/full/Agda/Interaction/Options.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE StandaloneDeriving, DeriveFunctor, CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE StandaloneDeriving #-}  module Agda.Interaction.Options     ( CommandLineOptions(..)
src/full/Agda/Interaction/Response.hs view
@@ -1,7 +1,10 @@ ------------------------------------------------------------------------ -- | Data type for all interactive responses -------------------------------------------------------------------------{-# LANGUAGE CPP, TypeSynonymInstances, FlexibleInstances #-}++{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.Interaction.Response   ( Response (..)
src/full/Agda/Main.hs view
@@ -18,6 +18,7 @@ import qualified Text.PrettyPrint.Boxes as Boxes  import Agda.Syntax.Concrete.Pretty ()+import Agda.Syntax.Abstract.Name (toTopLevelModuleName)  import Agda.Interaction.CommandLine.CommandLine import Agda.Interaction.Options@@ -142,13 +143,13 @@             NoWarnings -> return $ Just i            whenM (optGenerateHTML <$> commandLineOptions) $-            generateHTML $ iModuleName i+            generateHTML            whenM (isJust . optDependencyGraph <$> commandLineOptions) $             Dot.generateDot $ i            whenM (optGenerateLaTeX <$> commandLineOptions) $-            LaTeX.generateLaTeX (iModuleName i) (iHighlighting i)+            LaTeX.generateLaTeX (toTopLevelModuleName $ iModuleName i) (iHighlighting i)            return result
− src/full/Agda/Packaging/Config.hs 
@@ -1,23 +0,0 @@-module Agda.Packaging.Config where--- FIXME: proper exports--{---- External Library Imports-import qualified Distribution.InstalledPackageInfo-  as Cabal-    ( InstalledPackageInfo )---- Local Library Imports-import Agda.Packaging.Types-------------------------------------------------------------------------------------- Parametric in `opt' only so that the environment can be decoupled--- from the concrete CLI tool-data AgdaPkgConfig opt-  =  AgdaPkgConfig-  { configOpts       :: [opt]-  , configOrigBroken :: [Cabal.InstalledPackageInfo]-  , configPkgDBStack :: [NamedPackageDB]-  , configProgName   :: String }--}
− src/full/Agda/Packaging/Database.hs 
@@ -1,234 +0,0 @@-module Agda.Packaging.Database where--- FIXME: proper exports-{---- Standard Library Imports-import           Control.Applicative-import qualified Control.Exception-import           Control.Monad.Cont-import           Control.Monad.Error-import           Data.List-  ( foldl'-  , intersperse-  , isSuffixOf-  , partition )-import           Data.Maybe-  ( fromJust )-import           System.Directory-  ( createDirectoryIfMissing-  , getAppUserDataDirectory-  , getDirectoryContents-  , removeFile )-import           System.FilePath-import           System.IO-  ( IOMode (ReadMode)-  , hGetContents-  , hSetEncoding-  , openFile-  , utf8 )-import           System.IO.Error-  ( isPermissionError-  , try )---- External Library Imports-import qualified Distribution.InstalledPackageInfo-  as Cabal-    ( InstalledPackageInfo-    , exposed-    , exposedModules-    , depends-    , hiddenModules-    , installedPackageId-    , parseInstalledPackageInfo-    , showInstalledPackageInfo )-import qualified Distribution.Package-  as Cabal-    ( PackageIdentifier-    , packageId )-import qualified Distribution.ParseUtils-  as Cabal-    ( ParseResult (..)-    , locatedErrorMsg )-import qualified Distribution.Simple.Utils-  as Cabal-    ( die-    , writeUTF8File )-import qualified Distribution.Text-  as Cabal-    ( display-    , simpleParse )---- Local Imports-import Agda.Packaging.Config-import Agda.Packaging.Monad-import Agda.Packaging.Types-import Paths_Agda-  ( getDataDir )---------------------------------------------------------------------------------------------------------------- Getting the DB paths -------------------------------getPkgDBPathGlobal :: IO FilePath-getPkgDBPathGlobal = do-  result <- try action-  case result of-    Left  ioErr    -> Cabal.die $ show ioErr-    Right filePath -> return filePath-  where-    action =  pure (</>)-          <*> getDataDir-          <*> pure "package.conf.d"--getPkgDBPathUser :: IO FilePath-getPkgDBPathUser = do-  result <- try action-  case result of-    Left  ioErr    -> Cabal.die $ show ioErr-    Right filePath -> return filePath-  where-    action =  pure (</>)-          <*> getAppUserDataDirectory "Agda"-          <*> pure "package.conf.d"---------------------------------------- Loading the DBs into memory --------------------------------------getPkgDBs :: [FilePath] -> IO PackageDBStack-getPkgDBs givenPkgDBNames = do-  pkgDBNames <--    -- If no package databases are specified, default to getting the-    -- global and user packages.-    if null givenPkgDBNames-    then-          pure (\ db1 db2 -> db1 : db2 : [])-      <*> getPkgDBPathGlobal-      <*> getPkgDBPathUser-    else-      return givenPkgDBNames-  mapM readParsePkgDB pkgDBNames--readParsePkgDB :: PackageDBName -> IO NamedPackageDB-readParsePkgDB dbName = do-  result <- try $ getDirectoryContents dbName-  case result of-    Left  ioErr     -> Cabal.die $ show ioErr-    Right filePaths -> do-      pkgInfos <- mapM parseSingletonPkgConf $ map (dbName </>) dbEntries-      return $ NamedPackageDB-        { dbName = dbName-        , db     = pkgInfos }-      where-        dbEntries = filter (".conf" `isSuffixOf`) filePaths--parseSingletonPkgConf :: FilePath -> IO Cabal.InstalledPackageInfo-parseSingletonPkgConf = (parsePkgInfo =<<) . readUTF8File-  where-    readUTF8File :: FilePath -> IO String-    readUTF8File file = do-      handle <- openFile file ReadMode-      hSetEncoding handle utf8-      hGetContents handle--parsePkgInfo :: String -> IO Cabal.InstalledPackageInfo-parsePkgInfo pkgInfoStr =-  case Cabal.parseInstalledPackageInfo pkgInfoStr of-    Cabal.ParseOk     warnings pkgInfo ->-      return pkgInfo-    Cabal.ParseFailed err              ->-      case Cabal.locatedErrorMsg err of-        (Nothing     , msg) -> Cabal.die msg-        (Just  lineNo, msg) -> Cabal.die (show lineNo ++ ": " ++ msg)------------------------- DB operations ------------------------data DBOp-  = PkgAdd    Cabal.InstalledPackageInfo-  | PkgModify Cabal.InstalledPackageInfo-  | PkgRemove Cabal.InstalledPackageInfo---------------------------------------- Processing the DBs in memory ---------------------------------------brokenPkgs :: PackageDB -> PackageDB-brokenPkgs = snd . transClos []-  where-    -- Calculate the transitive closure of 'ok' packages, i.e.,-    -- packages with all of their dependencies available.-    transClos :: PackageDB -> PackageDB -> (PackageDB, PackageDB)-    transClos okPkgs pkgs =-      case partition (ok okPkgs) pkgs of-        ([]     , pkgs') -> (okPkgs, pkgs')-        (okPkgs', pkgs') -> transClos (okPkgs' ++ okPkgs) pkgs'-      where-        -- A package is 'ok' with respect to a package database if the-        -- packages dependencies are available in the database.-        ok :: PackageDB -> Cabal.InstalledPackageInfo -> Bool-        ok okPkgs pkg = null dangling-          where-            dangling = filter (`notElem` pkgIds) (Cabal.depends pkg)-            pkgIds   = map Cabal.installedPackageId okPkgs--flattenPkgDBs :: PackageDBStack -> PackageDB-flattenPkgDBs = concatMap db--modifyDBWithOps :: PackageDB -> [DBOp] -> PackageDB-modifyDBWithOps pkgDB dbOps = foldl' applyOp pkgDB dbOps-  where-    applyOp :: PackageDB -> DBOp -> PackageDB-    applyOp pkgInfos (PkgAdd    pkgInfo) = pkgInfo : pkgInfos-    applyOp pkgInfos (PkgModify pkgInfo) = applyOp pkgDB' $ PkgAdd pkgInfo-      where-        pkgDB' = applyOp pkgInfos $ PkgRemove pkgInfo-    applyOp pkgInfos (PkgRemove pkgInfo) = filter fpred pkgInfos-      where-        fpred  = (Cabal.installedPackageId pkgInfo /=)-               .  Cabal.installedPackageId------------------------------------- Modifying the DBs on disk ------------------------------------modifyAndWriteDBWithOps :: NamedPackageDB -> [DBOp] -> IO ()-modifyAndWriteDBWithOps npkgDB dbOps = do-  createDirectoryIfMissing True $ dbName npkgDB-  writeDBWithOps npkgDB{ db = db' } dbOps-  where-    db' = db npkgDB `modifyDBWithOps` dbOps--writeDBWithOps :: NamedPackageDB -> [DBOp] -> IO ()-writeDBWithOps npkgDB = mapM_ doOp-  where-    fileNameOf      pkgInfo  =  dbName npkgDB-                            </> Cabal.display (Cabal.installedPackageId pkgInfo)-                            <.> "conf"--    doOp (PkgAdd    pkgInfo) = Cabal.writeUTF8File (fileNameOf pkgInfo)-                             $ Cabal.showInstalledPackageInfo  pkgInfo-    doOp (PkgModify pkgInfo) = doOp                   $ PkgAdd pkgInfo-    doOp (PkgRemove pkgInfo) = removeFile          (fileNameOf pkgInfo)--modifyPkgInfoAndWriteDBWithFun :: Cabal.PackageIdentifier-                               -> (Cabal.InstalledPackageInfo -> DBOp)-                               -> AgdaPkg opt ()-modifyPkgInfoAndWriteDBWithFun pkgId funToOp = asksM (rec . configPkgDBStack)-  where-    rec :: PackageDBStack -> AgdaPkg opt ()-    rec = liftIO . mapM_ (\ npkgDB -> modifyAndWriteDBWithOps npkgDB (generateOps $ db npkgDB))-      where-        generateOps :: PackageDB -> [DBOp]-        generateOps []                       = []-        generateOps (pkgInfo:pkgInfos)-          | Cabal.packageId pkgInfo == pkgId = funToOp pkgInfo : generateOps pkgInfos-          | otherwise                        =                   generateOps pkgInfos--}
− src/full/Agda/Packaging/Monad.hs 
@@ -1,38 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}--module Agda.Packaging.Monad where--{--  ( module Control.Monad.Reader-  , AgdaPkg (..)-  , asksM ) where---- Standard Library Imports-import Control.Applicative-import Control.Monad.Error-import Control.Monad.Reader---- Local Imports-import Agda.Packaging.Config-------------------------------------------------------------------------------------- Parametric in `opt' only so that the environment can be decoupled--- from the concrete CLI tool-newtype AgdaPkg opt a-  =     AgdaPkg-  { runAgdaPkg :: ReaderT (AgdaPkgConfig opt) IO a }-  deriving-    ( Functor-    , Monad-    , MonadError IOError-    , MonadReader (AgdaPkgConfig opt)-    , MonadIO )--instance Applicative (AgdaPkg opt) where-  pure  = return-  (<*>) = ap--asksM :: (MonadReader r m) => (r -> m a) -> m a-asksM = join . asks--}
− src/full/Agda/Packaging/Types.hs 
@@ -1,20 +0,0 @@-module Agda.Packaging.Types where--{---- External Library Imports-import qualified Distribution.InstalledPackageInfo-  as Cabal-    ( InstalledPackageInfo )-----------------------------------------------------------------------------------type PackageDBName = FilePath-type PackageDB     = [Cabal.InstalledPackageInfo]--data NamedPackageDB-  =  NamedPackageDB-  { dbName :: PackageDBName-  , db     :: PackageDB }--type PackageDBStack = [NamedPackageDB]--}
src/full/Agda/Syntax/Abstract.hs view
@@ -1,7 +1,13 @@-{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,-             DeriveTraversable, CPP, TemplateHaskell,-             MultiParamTypeClasses, FlexibleInstances,-             TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeSynonymInstances #-}+ {-| The abstract syntax. This is what you get after desugaring and scope     analysis of the concrete syntax. The type checker works on abstract syntax,     producing internal syntax ("Agda.Syntax.Internal").@@ -14,11 +20,12 @@ import Prelude hiding (foldl, foldr) import Control.Arrow ((***), first, second) import Control.Applicative++import Data.Foldable as Fold+import Data.Map (Map) import Data.Sequence (Seq, (<|), (><)) import qualified Data.Sequence as Seq-import Data.Foldable as Fold import Data.Traversable-import Data.Map (Map) import Data.Typeable (Typeable)  import qualified Agda.Syntax.Concrete as C@@ -899,7 +906,7 @@     matchNext _ [] = False     matchNext n (a:as) = getHiding n == getHiding a && matchName       where-        x = unranged $ show $ nameConcrete $ unArg n+        x = unranged $ C.nameToRawName $ nameConcrete $ unArg n         matchName = maybe True (== x) (nameOf $ unArg a)      matchArgs r [] []     = return ([], [])
src/full/Agda/Syntax/Abstract/Copatterns.hs view
@@ -1,4 +1,13 @@-{-# LANGUAGE CPP, TupleSections, PatternGuards, DeriveFunctor, StandaloneDeriving, ScopedTypeVariables, TypeSynonymInstances, FlexibleContexts,  FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+ module Agda.Syntax.Abstract.Copatterns (translateCopatternClauses) where  import Prelude hiding (mapM)
src/full/Agda/Syntax/Abstract/Name.hs view
@@ -1,7 +1,11 @@-{-# LANGUAGE CPP,-  DeriveDataTypeable, GeneralizedNewtypeDeriving,-  DeriveFunctor, DeriveFoldable, DeriveTraversable,-  FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}  {-| Abstract names carry unique identifiers and stuff. -}@@ -116,14 +120,18 @@ noModuleName :: ModuleName noModuleName = mnameFromList [] --- | The 'Range' sets the /definition site/ of the name, not the use site.+-- | Make a 'Name' from some kind of string.+class MkName a where+  -- | The 'Range' sets the /definition site/ of the name, not the use site.+  mkName :: Range -> NameId -> a -> Name -mkName :: Range -> NameId -> String -> Name-mkName r i s = Name i (C.Name noRange (C.stringNameParts s)) r defaultFixity'+  mkName_ :: NameId -> a -> Name+  mkName_ = mkName noRange -mkName_ :: NameId -> String -> Name-mkName_ = mkName noRange+instance MkName String where+  mkName r i s = Name i (C.Name noRange (C.stringNameParts s)) r defaultFixity' + qnameToList :: QName -> [Name] qnameToList (QName m x) = mnameToList m ++ [x] @@ -193,9 +201,6 @@   i <- fresh   return $ mkName r i s -freshName_ :: (MonadState s m, HasFresh NameId s) => String -> m Name-freshName_ = freshName noRange- freshNoName :: (MonadState s m, HasFresh NameId s) => Range -> m Name freshNoName r =     do	i <- fresh@@ -203,6 +208,22 @@  freshNoName_ :: (MonadState s m, HasFresh NameId s) => m Name freshNoName_ = freshNoName noRange++-- | Create a fresh name from @a@.+class FreshName a where+  freshName_ :: (MonadState s m, HasFresh NameId s) => a -> m Name++instance FreshName (Range, String) where+  freshName_ = uncurry freshName++instance FreshName String where+  freshName_ = freshName noRange++instance FreshName Range where+  freshName_ = freshNoName++instance FreshName () where+  freshName_ () = freshNoName_  -- | Get the next version of the concrete name. For instance, @nextName "x" = "x₁"@. --   The name must not be a 'NoName'.
src/full/Agda/Syntax/Common.hs view
@@ -1,19 +1,30 @@-{-# LANGUAGE CPP, FlexibleInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving,-             DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}  {-| Some common syntactic entities are defined in this module. -} module Agda.Syntax.Common where  import Control.Applicative-import Data.Typeable (Typeable)++import Data.ByteString.Char8 (ByteString)+import qualified Data.ByteString.Char8 as ByteString import Data.Foldable-import Data.Traversable import Data.Hashable+import Data.Traversable+import Data.Typeable (Typeable)+ import Test.QuickCheck  import Agda.Syntax.Position+ import Agda.Utils.Functor+import Agda.Utils.Pretty import Agda.Utils.Size  #include "../undefined.h"@@ -337,6 +348,24 @@   zipWith (\x -> fmap (x <$)) xs args  ---------------------------------------------------------------------------+-- * Names+---------------------------------------------------------------------------++class Eq a => Underscore a where+  underscore   :: a+  isUnderscore :: a -> Bool+  isUnderscore = (== underscore)++instance Underscore String where+  underscore = "_"++instance Underscore ByteString where+  underscore = ByteString.pack underscore++instance Underscore Doc where+  underscore = text underscore++--------------------------------------------------------------------------- -- * Function type domain --------------------------------------------------------------------------- @@ -394,12 +423,16 @@ -- * Named arguments --------------------------------------------------------------------------- +-- | Something potentially carrying a name. data Named name a =     Named { nameOf     :: Maybe name 	  , namedThing :: a 	  }     deriving (Eq, Ord, Typeable, Functor, Foldable, Traversable) +-- | Standard naming.+type Named_ = Named RString+ unnamed :: a -> Named name a unnamed = Named Nothing @@ -418,12 +451,12 @@ instance Sized a => Sized (Named name a) where   size = size . namedThing -instance Show a => Show (Named RString a) where+instance Show a => Show (Named_ a) where     show (Named Nothing x)  = show x-    show (Named (Just n) x) = rangedThing n ++ " = " ++ show x+    show (Named (Just n) x) = rawNameToString (rangedThing n) ++ " = " ++ show x  -- | Only 'Hidden' arguments can have names.-type NamedArg c a = Arg c (Named RString a)+type NamedArg c a = Arg c (Named_ a)  -- | Get the content of a 'NamedArg'. namedArg :: NamedArg c a -> a@@ -470,8 +503,21 @@ instance Decoration Ranged where   traverseF f (Ranged r x) = Ranged r <$> f x +---------------------------------------------------------------------------+-- * Raw names (before parsing into name parts).+---------------------------------------------------------------------------++-- | A @RawName@ is some sort of string.+type RawName = String++rawNameToString :: RawName -> String+rawNameToString = id++stringToRawName :: String -> RawName+stringToRawName = id+ -- | String with range info.-type RString = Ranged String+type RString = Ranged RawName  --------------------------------------------------------------------------- -- * Infixity, access, abstract, etc.
src/full/Agda/Syntax/Concrete.hs view
@@ -1,4 +1,10 @@-{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveTraversable, DeriveFoldable, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  {-| The concrete syntax is a raw representation of the program text     without any desugaring at all.  This is what the parser produces.@@ -88,8 +94,8 @@ 	| App !Range Expr (NamedArg Expr)      -- ^ ex: @e e@, @e {e}@, or @e {x = e}@ 	| OpApp !Range QName [NamedArg (OpApp Expr)] -- ^ ex: @e + e@         | WithApp !Range Expr [Expr]           -- ^ ex: @e | e1 | .. | en@-	| HiddenArg !Range (Named RString Expr) -- ^ ex: @{e}@ or @{x=e}@-	| InstanceArg !Range (Named RString Expr) -- ^ ex: @{{e}}@ or @{{x=e}}@+	| HiddenArg !Range (Named_ Expr)       -- ^ ex: @{e}@ or @{x=e}@+	| InstanceArg !Range (Named_ Expr)     -- ^ ex: @{{e}}@ or @{{x=e}}@ 	| Lam !Range [LamBinding] Expr	       -- ^ ex: @\\x {y} -> e@ or @\\(x:A){y:B} -> e@         | AbsurdLam !Range Hiding              -- ^ ex: @\\ ()@         | ExtendedLam !Range [(LHS,RHS,WhereClause)]       -- ^ ex: @\\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }@@@ -123,8 +129,8 @@ 	| AppP Pattern (NamedArg Pattern)         -- ^ @p p'@ or @p {x = p'}@ 	| RawAppP !Range [Pattern]                -- ^ @p1..pn@ before parsing operators 	| OpAppP !Range QName [NamedArg Pattern]  -- ^ eg: @p => p'@ for operator @_=>_@-	| HiddenP !Range (Named RString Pattern)   -- ^ @{p}@ or @{x = p}@-	| InstanceP !Range (Named RString Pattern) -- ^ @{{p}}@ or @{{x = p}}@+	| HiddenP !Range (Named_ Pattern)         -- ^ @{p}@ or @{x = p}@+	| InstanceP !Range (Named_ Pattern)       -- ^ @{{p}}@ or @{{x = p}}@ 	| ParenP !Range Pattern                   -- ^ @(p)@ 	| WildP !Range                            -- ^ @_@ 	| AbsurdP !Range                          -- ^ @()@
src/full/Agda/Syntax/Concrete/Definitions.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards, DeriveDataTypeable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE PatternGuards #-}  module Agda.Syntax.Concrete.Definitions     ( NiceDeclaration(..)
src/full/Agda/Syntax/Concrete/Generic.hs view
@@ -3,7 +3,9 @@ -- --   However, here we use the terminology of 'Data.Traversable'. -{-# LANGUAGE CPP, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.Syntax.Concrete.Generic where
src/full/Agda/Syntax/Concrete/Name.hs view
@@ -1,6 +1,8 @@-{-# LANGUAGE CPP, PatternGuards,-  FlexibleInstances, TypeSynonymInstances,-  DeriveDataTypeable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}  {-| Names in the concrete syntax are just strings (or lists of strings for     qualified names).@@ -10,6 +12,8 @@ import Control.DeepSeq import Control.Applicative +import Data.ByteString.Char8 (ByteString)+import qualified Data.ByteString.Char8 as ByteString import Data.List import Data.Typeable (Typeable) @@ -40,11 +44,17 @@  instance NFData Name +instance Underscore Name where+  underscore = NoName noRange __IMPOSSIBLE__+  isUnderscore NoName{}        = True+  isUnderscore (Name _ [Id x]) = isUnderscore x+  isUnderscore _               = False+ -- | Mixfix identifiers are composed of words and holes, --   e.g. @_+_@ or @if_then_else_@ or @[_/_]@. data NamePart   = Hole       -- ^ @_@ part.-  | Id String  -- ^ Identifier part.+  | Id RawName  -- ^ Identifier part.   deriving (Typeable)  -- | Define equality on @Name@ to ignore range so same names in different@@ -90,6 +100,11 @@   | QName Name       -- ^ @x@.   deriving (Typeable, Eq, Ord) +instance Underscore QName where+  underscore = QName underscore+  isUnderscore (QName x) = isUnderscore x+  isUnderscore Qual{}    = False+ -- | Top-level module names.  Used in connection with the file system. -- --   Invariant: The list must not be empty.@@ -102,11 +117,14 @@ -- * Operations on 'Name' and 'NamePart' ------------------------------------------------------------------------ +nameToRawName :: Name -> RawName+nameToRawName = show+ nameParts :: Name -> [NamePart] nameParts (Name _ ps)  = ps nameParts (NoName _ _) = [Hole] -nameStringParts :: Name -> [String]+nameStringParts :: Name -> [RawName] nameStringParts n = [ s | Id s <- nameParts n ]  -- | Parse a string to parts of a concrete name.@@ -114,7 +132,7 @@ stringNameParts :: String -> [NamePart] stringNameParts ""                              = [] stringNameParts ('_':s)                         = Hole : stringNameParts s-stringNameParts s | (x, s') <- break (== '_') s = Id x : stringNameParts s'+stringNameParts s | (x, s') <- break (== '_') s = Id (stringToRawName x) : stringNameParts s'  -- | Is the name an operator? @@ -205,8 +223,11 @@   isNoName :: a -> Bool  instance IsNoName String where-  isNoName = (== "_")+  isNoName = isUnderscore +instance IsNoName ByteString where+  isNoName = isUnderscore+ instance IsNoName Name where   isNoName (NoName _ _)    = True   isNoName (Name _ [Hole]) = True   -- TODO: Track down where these come from@@ -229,7 +250,7 @@  instance Show NamePart where     show Hole   = "_"-    show (Id s) = s+    show (Id s) = rawNameToString s  instance Show QName where     show (Qual m x) = show m ++ "." ++ show x
src/full/Agda/Syntax/Concrete/Operators.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}  {-| The parser doesn't know about operators and parses everything as normal     function application. This module contains the functions that parses the
src/full/Agda/Syntax/Concrete/Operators/Parser.hs view
@@ -1,8 +1,10 @@-{-# LANGUAGE CPP, ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Agda.Syntax.Concrete.Operators.Parser where  import Control.Exception (throw)+ import Data.Maybe  import Agda.Syntax.Position@@ -23,8 +25,8 @@     | OtherV e     | AppV e (NamedArg e)     | OpAppV QName [NamedArg (OpApp e)]-    | HiddenArgV (Named RString e)-    | InstanceArgV (Named RString e)+    | HiddenArgV (Named_ e)+    | InstanceArgV (Named_ e)     | LamV [LamBinding] e     | ParenV e --    deriving (Show)@@ -51,7 +53,7 @@ -- Specific combinators  -- | Parse a specific identifier as a NamePart-partP :: IsExpr e => [Name] -> String -> ReadP e Range+partP :: IsExpr e => [Name] -> RawName -> ReadP e Range partP ms s = do     tok <- get     case isLocal tok of
src/full/Agda/Syntax/Concrete/Pretty.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE CPP, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}+ {-# OPTIONS -fno-warn-orphans #-}  {-| Pretty printer for the concrete syntax.@@ -57,7 +60,6 @@  arrow  = text "\x2192" lambda = text "\x03bb"-underscore = text "_"  pHidden :: Pretty a => ArgInfo -> a -> Doc pHidden i = bracks h . pretty@@ -471,9 +473,9 @@                -- TODO guilhem: print colors                pHidden (argInfo a) $ unArg a -instance Pretty e => Pretty (Named RString e) where+instance Pretty e => Pretty (Named_ e) where     pretty (Named Nothing e) = pretty e-    pretty (Named (Just s) e) = sep [ text (rangedThing s) <+> text "=", pretty e ]+    pretty (Named (Just s) e) = sep [ text (rawNameToString $ rangedThing s) <+> text "=", pretty e ]  instance Pretty [Pattern] where     pretty = fsep . map pretty
src/full/Agda/Syntax/Fixity.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+-- {-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}  {-| Definitions for fixity and precedence levels. -}
src/full/Agda/Syntax/Internal.hs view
@@ -1,8 +1,13 @@-{-# LANGUAGE CPP, DeriveDataTypeable, GeneralizedNewtypeDeriving,-             DeriveFunctor, DeriveFoldable, DeriveTraversable,-             TemplateHaskell,-             MultiParamTypeClasses, FlexibleInstances,-             TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.Syntax.Internal     ( module Agda.Syntax.Internal@@ -10,18 +15,20 @@     , module Agda.Utils.Pointer     ) where -import Prelude hiding (foldr, mapM)+import Prelude hiding (foldr, mapM, null)+ import Control.Arrow ((***)) import Control.Applicative import Control.Monad.Identity hiding (mapM) import Control.Monad.State hiding (mapM) import Control.Parallel-import Data.Typeable (Typeable)+ import Data.Foldable-import Data.Traversable import Data.Function-import Data.Maybe import qualified Data.List as List+import Data.Maybe+import Data.Traversable+import Data.Typeable (Typeable)  import Agda.Syntax.Position import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)@@ -29,12 +36,13 @@ import Agda.Syntax.Literal import Agda.Syntax.Abstract.Name +import Agda.Utils.Functor import Agda.Utils.Geniplate-import Agda.Utils.Size+import Agda.Utils.List+import Agda.Utils.Null import Agda.Utils.Permutation import Agda.Utils.Pointer-import Agda.Utils.List-import Agda.Utils.Functor+import Agda.Utils.Size  #include "../undefined.h" import Agda.Utils.Impossible@@ -126,14 +134,29 @@ type Elim = Elim' Term type Elims = [Elim]  -- ^ eliminations ordered left-to-right. +-- | Names in binders and arguments.+type ArgName = String++argNameToString :: ArgName -> String+argNameToString = id++stringToArgName :: String -> ArgName+stringToArgName = id++appendArgNames :: ArgName -> ArgName -> ArgName+appendArgNames = (++)++nameToArgName :: Name -> ArgName+nameToArgName = stringToArgName . show+ -- | Binder. --   'Abs': The bound variable might appear in the body. --   'NoAbs' is pseudo-binder, it does not introduce a fresh variable, --      similar to the @const@ of Haskell.-data Abs a = Abs   { absName :: String, unAbs :: a }+data Abs a = Abs   { absName :: ArgName, unAbs :: a }                -- ^ The body has (at least) one free variable.                --   Danger: 'unAbs' doesn't shift variables properly-           | NoAbs { absName :: String, unAbs :: a }+           | NoAbs { absName :: ArgName, unAbs :: a }   deriving (Typeable, Functor, Foldable, Traversable)  -- | Types are terms with a sort annotation.@@ -154,14 +177,14 @@  type Telescope = Tele (Dom Type) -mapAbsNamesM :: Applicative m => (String -> m String) -> Tele a -> m (Tele a)+mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) mapAbsNamesM f EmptyTel                  = pure EmptyTel mapAbsNamesM f (ExtendTel a (Abs x b))   = ExtendTel a <$> (Abs <$> f x <*> mapAbsNamesM f b) mapAbsNamesM f (ExtendTel a (NoAbs x b)) = ExtendTel a <$> (NoAbs <$> f x <*> mapAbsNamesM f b)   -- Ulf, 2013-11-06: Last case is really impossible but I'd rather find out we   --                  violated that invariant somewhere other than here. -mapAbsNames :: (String -> String) -> Tele a -> Tele a+mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a mapAbsNames f = runIdentity . mapAbsNamesM (Identity . f)  -- Ulf, 2013-11-06@@ -172,10 +195,8 @@ -- TypeChecking.Monad.Signature.addConstant (to handle functions defined in -- record modules) and TypeChecking.Rules.Record.checkProjection (to handle -- record projections).-replaceEmptyName :: String -> Tele a -> Tele a-replaceEmptyName x = mapAbsNames repl-  where repl "" = x-        repl y  = y+replaceEmptyName :: ArgName -> Tele a -> Tele a+replaceEmptyName x = mapAbsNames $ \ y -> if null y then x else y  -- | Sorts. --@@ -188,9 +209,10 @@             --   it's the normal Lub   deriving (Typeable, Show) --- | A level is a maximum expression of 0..n plus expressions+-- | A level is a maximum expression of 0..n 'PlusLevel' expressions --   each of which is a number or an atom plus a number. --+--   The empty maximum is the canonical representation for level 0. newtype Level = Max [PlusLevel]   deriving (Show, Typeable) @@ -285,6 +307,15 @@ instance HasRange Clause where   getRange = clauseRange +-- | Pattern variables.+type PatVarName = ArgName++patVarNameToString :: PatVarName -> String+patVarNameToString = argNameToString++nameToPatVarName :: Name -> PatVarName+nameToPatVarName = nameToArgName+ -- | Patterns are variables, constructors, or wildcards. --   @QName@ is used in @ConP@ rather than @Name@ since --     a constructor might come from a particular namespace.@@ -292,8 +323,8 @@ --     the arguments we are matching with) use @QName@. -- data Pattern-  = VarP String-    -- ^ The @String@ is a name suggestion.+  = VarP PatVarName+    -- ^ The @PatVarName@ is a name suggestion.   | DotP Term   | ConP ConHead ConPatternInfo [NamedArg Pattern]     -- ^ The @Pattern@s do not contain any projection copatterns.@@ -302,9 +333,9 @@     -- ^ Projection copattern.  Can only appear by itself.   deriving (Typeable, Show) -namedVarP :: String -> Named RString Pattern-namedVarP "_" = Named Nothing (VarP "_")-namedVarP x   = Named (Just $ unranged x) (VarP x)+namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern+namedVarP x = Named named $ VarP x+  where named = if isUnderscore x then Nothing else Just $ unranged x  -- | The @ConPatternInfo@ states whether the constructor belongs to --   a record type (@Just@) or data type (@Nothing@).@@ -317,7 +348,7 @@  -- | Extract pattern variables in left-to-right order. --   A 'DotP' is also treated as variable (see docu for 'Clause').-patternVars :: Arg Pattern -> [Arg (Either String Term)]+patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)] patternVars (Common.Arg i (VarP x)     ) = [Common.Arg i $ Left x] patternVars (Common.Arg i (DotP t)     ) = [Common.Arg i $ Right t] patternVars (Common.Arg i (ConP _ _ ps)) = List.concat $ map (patternVars . fmap namedThing) ps@@ -340,12 +371,18 @@ -- | Absurd lambdas are internally represented as identity --   with variable name "()". absurdBody :: Abs Term-absurdBody = Abs "()" $ Var 0 []+absurdBody = Abs absurdPatternName $ Var 0 []  isAbsurdBody :: Abs Term -> Bool-isAbsurdBody (Abs "()" (Var 0 [])) = True-isAbsurdBody _                     = False+isAbsurdBody (Abs x (Var 0 [])) = isAbsurdPatternName x+isAbsurdBody _                  = False +absurdPatternName :: PatVarName+absurdPatternName = "()"++isAbsurdPatternName :: PatVarName -> Bool+isAbsurdPatternName x = x == absurdPatternName+ --------------------------------------------------------------------------- -- * Pointers and Sharing ---------------------------------------------------------------------------@@ -460,7 +497,7 @@   , "Location of the error: " ++ file ++ ":" ++ show line   ] -sgTel :: Dom (String, Type) -> Telescope+sgTel :: Dom (ArgName, Type) -> Telescope sgTel (Common.Dom ai (x, t)) = ExtendTel (Common.Dom ai t) $ Abs x EmptyTel  ---------------------------------------------------------------------------@@ -501,7 +538,7 @@ argName :: Type -> String argName = argN . ignoreSharing . unEl     where-	argN (Pi _ b)  = "." ++ absName b+	argN (Pi _ b)  = "." ++ argNameToString (absName b) 	argN _	  = __IMPOSSIBLE__  -- | Pick the better name suggestion, i.e., the one that is not just underscore.
src/full/Agda/Syntax/Internal/Generic.hs view
@@ -1,5 +1,6 @@ -- {-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.Syntax.Internal.Generic where
src/full/Agda/Syntax/Internal/Pattern.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, FlexibleInstances, OverlappingInstances  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverlappingInstances #-}  module Agda.Syntax.Internal.Pattern where
src/full/Agda/Syntax/Notation.hs view
@@ -1,11 +1,12 @@-{-# LANGUAGE CPP, DeriveDataTypeable #-}-+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}  module Agda.Syntax.Notation where  import Control.Applicative import Control.Monad import Control.Monad.Error (throwError)+ import Data.List import Data.Maybe import Data.Typeable (Typeable)@@ -26,8 +27,8 @@  -- | Data type constructed in the Happy parser; converted to 'GenPart' -- before it leaves the Happy code.-data HoleName = LambdaHole String String -- ^ (\x -> y) ; 1st argument is the bound name (unused for now)-              | ExprHole String          -- ^ simple named hole with hiding+data HoleName = LambdaHole RawName RawName -- ^ (\x -> y) ; 1st argument is the bound name (unused for now)+              | ExprHole RawName           -- ^ simple named hole with hiding  -- | Target of a hole holeName (LambdaHole _ n) = n@@ -38,11 +39,11 @@ -- | Part of a Notation data GenPart = BindHole Int                 -- ^ Argument is the position of the hole (with binding) where the binding should occur.              | NormalHole (NamedArg () Int) -- ^ Argument is where the expression should go-             | IdPart String+             | IdPart RawName   deriving (Typeable, Show, Eq)  -- | Get a flat list of identifier parts of a notation.-stringParts :: Notation -> [String]+stringParts :: Notation -> [RawName] stringParts gs = [ x | IdPart x <- gs ]  -- | Target argument position of a part (Nothing if it is not a hole)@@ -63,7 +64,7 @@   -- | From notation with names to notation with indices.-mkNotation :: [NamedArg c HoleName] -> [String] -> Either String Notation+mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String Notation mkNotation _ [] = throwError "empty notation is disallowed" mkNotation holes ids = do   unless (uniqueNames holes) $ throwError "syntax must use unique argument names"
src/full/Agda/Syntax/Parser/Layout.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP #-}+-- {-# LANGUAGE CPP #-}  {-| This module contains the lex actions that handle the layout rules. The way     it works is that the 'Parser' monad keeps track of a stack of
src/full/Agda/Syntax/Parser/Parser.y view
@@ -1,7 +1,4 @@ {-{-# OPTIONS_GHC -fno-warn-incomplete-patterns-                -fno-warn-deprecated-flags #-}-{-# LANGUAGE BangPatterns, PatternGuards #-} {-| The parser is generated by Happy (<http://www.haskell.org/happy>).  -  - Ideally, ranges should be as precise as possible, to get messages that@@ -23,7 +20,9 @@     ) where  import Control.Monad+ import Data.Char+import Data.Functor import Data.List import Data.Maybe import qualified Data.Traversable as T@@ -1084,7 +1083,7 @@  -- Discard the interval. SimpleId :: { RString }-SimpleId : id  { Ranged (getRange $ fst $1) (snd $1) }+SimpleId : id  { Ranged (getRange $ fst $1) (stringToRawName $ snd $1) }  MaybeOpen :: { Maybe Range } MaybeOpen : 'open'      { Just (getRange $1) }@@ -1100,12 +1099,12 @@     ; dir = $5     ; r   = getRange (m, es, dir)     ; mr  = getRange m-    ; unique = hashString $ show $ fmap (const (Nothing :: Maybe ())) r+    ; unique = hashString $ show $ (Nothing :: Maybe ()) <$ r          -- turn range into unique id, but delete file path          -- which is absolute and messes up suite of failing tests          -- (different hashs on different installations)          -- TODO: Don't use (insecure) hashes in this way.-    ; fresh = Name mr [ Id $ ".#" ++ show m ++ "-" ++ show unique ]+    ; fresh = Name mr [ Id $ stringToRawName $ ".#" ++ show m ++ "-" ++ show unique ]     ; impStm asR = Import mr m (Just (AsName fresh asR)) DontOpen defaultImportDir     ; appStm m' es =         let r = getRange (m, es) in@@ -1119,7 +1118,7 @@     ; parseAsClause = case last2Args of       { [ Ident (QName (Name asR [Id x]))         , Ident (QName m')-        ] | x == "as" -> Just (asR, m')+        ] | rawNameToString x == "as" -> Just (asR, m')       ; _ -> Nothing       }     } in@@ -1427,7 +1426,9 @@     return $ Name (getRange i) xs     where 	isValidId Hole   = return ()-	isValidId (Id x) = case parse defaultParseFlags [0] (lexer return) x of+	isValidId (Id y) = do+          let x = rawNameToString y+          case parse defaultParseFlags [0] (lexer return) x of 	    ParseOk _ (TokId _) -> return () 	    _			-> fail $ "in the name " ++ s ++ ", the part " ++ x ++ " is not valid" @@ -1601,10 +1602,10 @@     Equal _ a b -> Just (stripSingletonRawApp a, stripSingletonRawApp b)     _           -> Nothing -maybeNamed :: Expr -> Named RString Expr+maybeNamed :: Expr -> Named_ Expr maybeNamed e =   case isEqual e of-    Just (Ident (QName x), b) -> named (Ranged (getRange x) (show x)) b+    Just (Ident (QName x), b) -> named (Ranged (getRange x) (nameToRawName x)) b     _                         -> unnamed e  patternSynArgs :: [Either Hiding LamBinding] -> Parser [Arg Name]
src/full/Agda/Syntax/Position.hs view
@@ -68,12 +68,12 @@ import Control.Monad  import Data.Foldable (Foldable)-import Data.Traversable (Traversable) import Data.Function import Data.Int import Data.List import Data.Set (Set) import qualified Data.Set as Set+import Data.Traversable (Traversable) import Data.Typeable (Typeable)  import Test.QuickCheck.All@@ -491,8 +491,8 @@  instance Arbitrary a => Arbitrary (Position' a) where   arbitrary = do-    srcFile                    <- arbitrary-    NonZero (NonNegative pos') <- arbitrary+    srcFile       <- arbitrary+    Positive pos' <- arbitrary     let pos  = fromInteger pos'         line = pred pos `div` 10 + 1         col  = pred pos `mod` 10 + 1
src/full/Agda/Syntax/Scope/Base.hs view
@@ -1,4 +1,10 @@-{-# LANGUAGE CPP, DeriveDataTypeable, GADTs, ScopedTypeVariables, TupleSections, RankNTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TupleSections #-}+  {-| This module defines the notion of a scope and operations on scopes. -}
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs view
@@ -1,8 +1,13 @@ -- {-# OPTIONS -fwarn-unused-binds #-}-{-# LANGUAGE CPP, PatternGuards, MultiParamTypeClasses, FunctionalDependencies,-             TypeSynonymInstances, FlexibleInstances, UndecidableInstances-  #-} +{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}+ {-| The translation of abstract syntax to concrete syntax has two purposes.     First it allows us to pretty print abstract syntax values without having to     write a dedicated pretty printer, and second it serves as a sanity check@@ -23,13 +28,15 @@     , noTakenNames     ) where -import Control.Applicative+import Prelude hiding (null)++import Control.Applicative hiding (empty) import Control.Monad.Reader +import Data.List as List hiding (null) import qualified Data.Map as Map import qualified Data.Set as Set import Data.Set (Set)-import Data.List as List import Data.Traversable (traverse)  import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)@@ -48,6 +55,7 @@ import Agda.TypeChecking.Monad.Options  import Agda.Utils.Monad hiding (bracket)+import Agda.Utils.Null import Agda.Utils.Tuple  #include "../../undefined.h"@@ -166,9 +174,9 @@     Just y  -> return y     Nothing -> do       let y = qnameToConcrete x-      if show y == "_"+      if isUnderscore y         then return y-        else return $ C.Qual (C.Name noRange [Id ""]) y+        else return $ C.Qual (C.Name noRange [Id empty]) y         -- this is what happens for names that are not in scope (private names)  lookupModule :: A.ModuleName -> AbsToCon C.QName@@ -874,7 +882,7 @@         e <- toConcreteCtx DotPatternCtx e         return $ C.DotP (getRange i) e     -- just for debugging purposes (shouldn't show up in practise)-    toConcrete (A.ImplicitP i) = return $ C.IdentP (C.QName $ C.Name noRange [C.Id "(implicit)"])+    toConcrete (A.ImplicitP i) = return $ C.IdentP (C.QName $ C.Name noRange [C.Id $ stringToRawName "(implicit)"])     toConcrete (A.PatternSynP i n _) = IdentP <$> toConcrete n  @@ -935,7 +943,7 @@   doQName _ n es     | length xs == 1        = mDefault     | length es /= numHoles = mDefault-    | List.null es          = mDefault+    | null es               = mDefault     where       xs       = C.nameParts $ C.unqualify n       numHoles = length (filter (== Hole) xs)
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs view
@@ -1,7 +1,11 @@-{-# LANGUAGE CPP, MultiParamTypeClasses, FunctionalDependencies,-             FlexibleInstances, UndecidableInstances, OverlappingInstances,-             ScopedTypeVariables, TypeSynonymInstances-  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}  {-| Translation from "Agda.Syntax.Concrete" to "Agda.Syntax.Abstract". Involves scope analysis,     figuring out infix operator precedences and tidying up definitions.@@ -598,7 +602,7 @@           where             nextlamname :: Range -> Int -> String -> ScopeM C.Name             nextlamname r i s = do-              let cname_pre = C.Name r [Id $ s ++ show i]+              let cname_pre = C.Name r [Id $ stringToRawName $ s ++ show i]               rn <- resolveName (C.QName cname_pre)               case rn of                 UnknownName -> return $ cname_pre@@ -866,7 +870,7 @@         (ds', [C.Module r m0 tel ds]) -> do           -- If the module name is _ compute the name from the file path           m <- if isNoName m0-                then return $ C.QName $ C.Name noRange [Id $ rootName file]+                then return $ C.QName $ C.Name noRange [Id $ stringToRawName $ rootName file]                 else do                 -- Andreas, 2014-03-28  Issue 1078                 -- We need to check the module name against the file name here.
src/full/Agda/Syntax/Translation/InternalToAbstract.hs view
@@ -1,7 +1,12 @@-{-# LANGUAGE CPP, MultiParamTypeClasses, FunctionalDependencies,-             UndecidableInstances, TypeSynonymInstances, FlexibleInstances,-             ScopedTypeVariables, TupleSections, FlexibleContexts-  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}  {-|     Translating from internal syntax to abstract syntax. Enables nice@@ -27,14 +32,14 @@ import Control.Monad.Error hiding (mapM_, mapM) import Control.Monad.Reader hiding (mapM_, mapM) -import qualified Data.Set as Set-import Data.Set (Set)-import qualified Data.Map as Map+import Data.Foldable (foldMap) import Data.List hiding (sort)-import Data.Traversable as Trav+import qualified Data.Map as Map import Data.Maybe import Data.Monoid-import Data.Foldable (foldMap)+import Data.Set (Set)+import qualified Data.Set as Set+import Data.Traversable as Trav  import Agda.Syntax.Literal import Agda.Syntax.Position@@ -98,8 +103,9 @@ exprInfo :: ExprInfo exprInfo = ExprRange noRange -underscore :: Expr-underscore = A.Underscore $ Info.emptyMetaInfo+instance Underscore Expr where+  underscore   = A.Underscore $ Info.emptyMetaInfo+  isUnderscore = __IMPOSSIBLE__  -- Conditional reification to omit terms that are not shown -------------- @@ -495,7 +501,7 @@            napps (A.Def x `apps` pad) =<< reifyIArgs vs  -- | @nameFirstIfHidden n (a1->...an->{x:a}->b) ({e} es) = {x = e} es@-nameFirstIfHidden :: [I.Dom (String, t)] -> [I.Arg a] -> [I.NamedArg a]+nameFirstIfHidden :: [I.Dom (ArgName, t)] -> [I.Arg a] -> [I.NamedArg a] nameFirstIfHidden _         []                    = [] nameFirstIfHidden []        (_ : _)               = __IMPOSSIBLE__ nameFirstIfHidden (dom : _) (Common.Arg info e : es) | isHidden info =@@ -878,9 +884,9 @@                   a <- reify a                   return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)                 I.Prop       -> return $ A.Prop exprInfo-                I.Inf       -> A.Var <$> freshName_ "Setω"+                I.Inf       -> A.Var <$> freshName_ ("Setω" :: String)                 I.DLub s1 s2 -> do-                  lub <- freshName_ "dLub" -- TODO: hack+                  lub <- freshName_ ("dLub" :: String) -- TODO: hack                   (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)                   let app x y = A.App exprInfo x (defaultNamedArg y)                   return $ A.Var lub `app` e1 `app` e2@@ -895,7 +901,7 @@      -- If the bound variable is free in the body, then the name "_" is     -- replaced by "z".-    s <- return $ if s == "_" && 0 `freeIn` v then "z" else s+    s <- return $ if isUnderscore s && 0 `freeIn` v then "z" else s      x <- freshName_ s     e <- addCtx x dummyDom -- type doesn't matter
src/full/Agda/Termination/CallGraph.hs view
@@ -1,7 +1,14 @@-{-# LANGUAGE CPP, TupleSections, ImplicitParams,-  TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses,-  GeneralizedNewtypeDeriving, StandaloneDeriving, DeriveFunctor,-  DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | Call graphs and related concepts, more or less as defined in --     \"A Predicative Analysis of Structural Recursion\" by
src/full/Agda/Termination/CallMatrix.hs view
@@ -1,7 +1,13 @@-{-# LANGUAGE CPP, ImplicitParams, TypeSynonymInstances, FlexibleInstances,-  MultiParamTypeClasses,-  GeneralizedNewtypeDeriving, StandaloneDeriving, DeriveFunctor,-  DeriveFoldable, DeriveTraversable #-}+-- {-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.Termination.CallMatrix where
src/full/Agda/Termination/Inlining.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+ -- Author:  Ulf Norell -- Created: 2013-11-09 @@ -182,7 +184,7 @@     rebindBody n b = bind n $ maybe NoBody Body $ getBodyUnraised b       where         bind 0 = id-        bind n = Bind . Abs ("h" ++ show n') . bind n'+        bind n = Bind . Abs (stringToArgName $ "h" ++ show n') . bind n'           where n' = n - 1      dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)@@ -211,7 +213,7 @@         DDef{}           -> DotP (dtermToTerm v) <$ skip         DDot v           -> DotP v <$ skip         DTerm (Var i []) ->-          ifM (bindVar i) (VarP . show <$> lift (nameOfBV i))+          ifM (bindVar i) (VarP . nameToPatVarName <$> lift (nameOfBV i))                           (pure $ DotP (Var i []))         DTerm (Con c vs) -> ConP c Nothing . map (fmap unnamed) <$> mapM (traverse (dtermToPat . DTerm)) vs         DTerm v          -> DotP v <$ skip
src/full/Agda/Termination/Monad.hs view
@@ -1,5 +1,10 @@-{-# LANGUAGE CPP, FlexibleInstances, TypeSynonymInstances, MultiParamTypeClasses,-      DeriveFunctor, GeneralizedNewtypeDeriving, StandaloneDeriving #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | The monad for the termination checker. --@@ -21,18 +26,20 @@ import Agda.Interaction.Options (defaultCutOff)  import Agda.Syntax.Abstract (QName,IsProjP(..))-import Agda.Syntax.Common   (Delayed(..))+import Agda.Syntax.Common   (Delayed(..), Induction(..), Dom(..)) import Agda.Syntax.Internal import Agda.Syntax.Literal import Agda.Syntax.Position (noRange)  import Agda.Termination.CutOff import Agda.Termination.Order (Order,le,unknown)+import Agda.Termination.RecCheck (anyDefs)  import Agda.TypeChecking.Monad import Agda.TypeChecking.Monad.Builtin import Agda.TypeChecking.Pretty import Agda.TypeChecking.Records+import Agda.TypeChecking.Substitute  import Agda.Utils.Maybe import Agda.Utils.Monad@@ -291,10 +298,11 @@  -- | Set 'terUseSizeLt' for arguments following projection @q@. projUseSizeLt :: QName -> TerM a -> TerM a-projUseSizeLt q m = do-  ifM (liftTCM $ isProjectionButNotCoinductive q)-    (terSetUseSizeLt False m)-    (terSetUseSizeLt True  m)+projUseSizeLt q m = isCoinductiveProjection q >>= (`terSetUseSizeLt` m)+-- projUseSizeLt q m = do+--   ifM (liftTCM $ isProjectionButNotCoinductive q)+--     (terSetUseSizeLt False m)+--     (terSetUseSizeLt True  m)  -- | For termination checking purposes flat should not be considered a --   projection. That is, it flat doesn't preserve either structural order@@ -317,9 +325,42 @@         else do           mp <- isProjection qn           case mp of-            Just Projection{ projProper = Just{}, projFromType = t}+            Just Projection{ projProper = Just{}, projFromType = t }               -> isInductiveRecord t             _ -> return False++-- | Check whether a projection belongs to a coinductive record+--   and is actually recursive.+--   E.g.+--   @+--      isCoinductiveProjection (Stream.head) = return False+--+--      isCoinductiveProjection (Stream.tail) = return True+--   @+isCoinductiveProjection :: MonadTCM tcm => QName -> tcm Bool+isCoinductiveProjection q = liftTCM $ do+  flat <- fmap nameOfFlat <$> coinductionKit+  -- yes for ♭+  if Just q == flat then return True else do+  pdef <- getConstInfo q+  case isProjection_ (theDef pdef) of+    Just Projection{ projProper = Just{}, projFromType = r, projIndex = n }+      -> caseMaybeM (isRecord r) __IMPOSSIBLE__ $ \ rdef -> do+           -- no for inductive or non-recursive record+           if recInduction rdef == Inductive then return False else do+           if not (recRecursive rdef) then return False else do+           -- TODO: the following test for recursiveness of a projection should be cached.+           -- E.g., it could be stored in the @Projection@ component.+           -- Now check if type of field mentions mutually recursive symbol.+           -- Get the type of the field by dropping record parameters and record argument.+           let TelV tel core = telView' (defType pdef)+               tel' = drop n $ telToList tel+           -- Check if any recursive symbols appear in the record type.+           -- Q (2014-07-01): Should we normalize the type?+           names <- anyDefs (r : recMutual rdef) (map (snd . unDom) tel', core)+           return $ not $ null names+    _ -> return False+  -- * De Bruijn patterns.
src/full/Agda/Termination/Order.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE CPP, ImplicitParams, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | An Abstract domain of relative sizes, i.e., differences --   between size of formal function parameter and function argument
src/full/Agda/Termination/RecCheck.hs view
@@ -7,10 +7,13 @@      when there's no (co)recursion     Original contribution by Andrea Vezzosi (sanzhiyan).+   This implementation by Andreas. -}  module Agda.Termination.RecCheck-    ( recursive )+    ( recursive+    , anyDefs+    )  where  import Control.Applicative@@ -43,14 +46,19 @@   -- Retrieve definition   def <- getConstInfo name   case theDef def of-    Function{ funClauses = cls } -> do-      -- Prepare function to lookup metas outside of TCM-      st <- getMetaStore-      let lookup x = case mvInstantiation <$> Map.lookup x st of-            Just (InstV v) -> Just v-            _              -> Nothing-          -- we collect only those used definitions that are in @names@-          emb d = if d `elem` names then [d] else []-      -- get all the Defs that are in names-      return $ getDefs' lookup emb cls+    Function{ funClauses = cls } -> anyDefs names cls     _ -> return []++-- | @anysDef names a@ returns all definitions from @names@+--   that are used in @a@.+anyDefs :: GetDefs a => [QName] -> a -> TCM [QName]+anyDefs names a = do+  -- Prepare function to lookup metas outside of TCM+  st <- getMetaStore+  let lookup x = case mvInstantiation <$> Map.lookup x st of+        Just (InstV v) -> Just v+        _              -> Nothing+      -- we collect only those used definitions that are in @names@+      emb d = if d `elem` names then [d] else []+  -- get all the Defs that are in names+  return $ getDefs' lookup emb a
src/full/Agda/Termination/SparseMatrix.hs view
@@ -1,6 +1,13 @@-{-# LANGUAGE CPP, ScopedTypeVariables, TupleSections, NamedFieldPuns,-  MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,-  DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}  {- | Sparse matrices. @@ -687,7 +694,7 @@ -- | Matrix multiplication is well-defined and associative.  prop_mul sz =-  divPropSize 2 $+  mapSize (`div` 2) $   forAll (two natural) $ \(c2, c3) ->   forAll (matrix sz :: Gen TM) $ \m1 ->   forAll (matrix (Size { rows = cols sz, cols = c2 })) $ \m2 ->
src/full/Agda/Termination/TermCheck.hs view
@@ -1,6 +1,13 @@-{-# LANGUAGE CPP, PatternGuards, ImplicitParams, TupleSections, NamedFieldPuns,-             FlexibleInstances, TypeSynonymInstances,-             StandaloneDeriving, GeneralizedNewtypeDeriving, DeriveFunctor #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  {- Checking for Structural recursion    Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell,@@ -619,10 +626,10 @@   where     toPat (Common.Arg (Common.ArgInfo h r c) x) =            Common.Arg (Common.ArgInfo h r []) $ namedVarP x-    removeHiddenLambdas :: ClauseBody -> ([I.Arg String], ClauseBody)+    removeHiddenLambdas :: ClauseBody -> ([I.Arg ArgName], ClauseBody)     removeHiddenLambdas = underBinds $ hlamsToBinds -    hlamsToBinds :: Term -> ([I.Arg String], ClauseBody)+    hlamsToBinds :: Term -> ([I.Arg ArgName], ClauseBody)     hlamsToBinds v =       case ignoreSharing v of         Lam info b | getHiding info == Hidden ->@@ -792,10 +799,8 @@     -- then preserve guardedness for its principal argument.     isProj <- isProjectionButNotCoinductive g     let unguards = repeat Order.unknown-    let guards = if isProj then guarded : unguards-                                -- proj => preserve guardedness of principal argument-                           else unguards -- not a proj ==> unguarded-    -- collect calls in the arguments of this call+    let guards = applyWhen isProj (guarded :) unguards+    -- Collect calls in the arguments of this call.     let args = map unArg $ argsFromElims es     calls <- forM' (zip guards args) $ \ (guard, a) -> do       terSetGuarded guard $ extract a@@ -909,7 +914,7 @@       -- Dependent function space.       Pi a (Abs x b) -> CallGraph.union <$> (terUnguarded $ extract a) <*> do          a <- maskSizeLt a  -- OR: just do not add a to the context!-         terPiGuarded $ addCtxString x a $ terRaise $ extract b+         terPiGuarded $ addContext (x, a) $ terRaise $ extract b        -- Non-dependent function space.       Pi a (NoAbs _ b) -> CallGraph.union@@ -984,9 +989,11 @@    -- Count the number of coinductive projection(pattern)s in caller and callee   projsCaller <- genericLength <$> do-    filterM (not <.> isProjectionButNotCoinductive) $ mapMaybe isProjP pats+    filterM isCoinductiveProjection $ mapMaybe isProjP pats+    -- filterM (not <.> isProjectionButNotCoinductive) $ mapMaybe isProjP pats   projsCallee <- genericLength <$> do-    filterM (not <.> isProjectionButNotCoinductive) $ mapMaybe isProjElim es+    filterM isCoinductiveProjection $ mapMaybe isProjElim es+    -- filterM (not <.> isProjectionButNotCoinductive) $ mapMaybe isProjElim es   cutoff <- terGetCutOff   let ?cutoff = cutoff   let guardedness = decr $ projsCaller - projsCallee@@ -1143,7 +1150,7 @@         (:) <$> (Apply <$> stripAllProjections a) <*> stripAllProjections es       (Proj p  : es) -> do         isP <- isProjectionButNotCoinductive p-        (if isP then id else (Proj p :)) <$> stripAllProjections es+        applyUnless isP (Proj p :) <$> stripAllProjections es  instance StripAllProjections Args where   stripAllProjections = mapM stripAllProjections
src/full/Agda/Termination/Termination.hs view
@@ -25,7 +25,7 @@ import Agda.Utils.Either import Agda.Utils.List import Agda.Utils.Maybe-import Agda.Utils.TestHelpers+import Agda.Utils.TestHelpers hiding (idempotent) import Agda.Utils.QuickCheck  import qualified Data.Array as Array
+ src/full/Agda/TheTypeChecker.hs view
@@ -0,0 +1,8 @@++module Agda.TheTypeChecker+  ( checkDecls, checkDecl+  , inferExpr, checkExpr+  ) where++import Agda.TypeChecking.Rules.Decl+import Agda.TypeChecking.Rules.Term
− src/full/Agda/TypeChecker.hs 
@@ -1,8 +0,0 @@--module Agda.TypeChecker-  ( checkDecls, checkDecl-  , inferExpr, checkExpr-  ) where--import Agda.TypeChecking.Rules.Decl-import Agda.TypeChecking.Rules.Term
src/full/Agda/TypeChecking/Abstract.hs view
@@ -1,5 +1,7 @@ -- {-# LANGUAGE CPP #-}-{-# LANGUAGE PatternGuards, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | Functions for abstracting terms over other terms. module Agda.TypeChecking.Abstract where
src/full/Agda/TypeChecking/CheckInternal.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}+ -- Initially authored by Andreas, 2013-10-22.  -- | A bidirectional type checker for internal syntax.@@ -61,7 +65,7 @@     Pi a b -> do       s1 <- checkType' $ unDom a       s2 <- (b $>) <$> do-        addCtxString (absName b) a $ do+        addContext (absName b, a) $ do           checkType' $ absBody b       return $ dLub s1 s2     Sort s -> do@@ -121,13 +125,13 @@     Lam ai vb  -> do       (a, b) <- shouldBePi t       checkArgInfo ai $ domInfo a-      addCtxString (suggest vb b) a $ do+      addContext (suggest vb b, a) $ do         checkInternal (absBody vb) (absBody b)     Pi a b     -> do       s <- shouldBeSort t       let st = sort s       checkInternal (unEl $ unDom a) st-      addCtxString (absName b) a $ do+      addContext (absName b, a) $ do         checkInternal (unEl $ absBody b) $ raise 1 st     Sort s     -> do       checkSort s  -- this ensures @s /= Inf@@@ -289,7 +293,7 @@       -- we cannot have Setω on the lhs of the colon     DLub a b -> do       checkSort a-      addCtxString (absName b) (defaultDom (sort a)) $ do+      addContext (absName b, defaultDom (sort a) :: I.Dom Type) $ do         checkSort (absBody b)  -- | Check if level is well-formed.
src/full/Agda/TypeChecking/CompiledClause.hs view
@@ -1,4 +1,10 @@-{-# LANGUAGE TypeOperators, CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TypeOperators #-}+ module Agda.TypeChecking.CompiledClause where  import qualified Data.Map as Map@@ -41,7 +47,7 @@     -- ^ @CoCase n bs@ matches on projections.     --   Catch-all is not meaningful here. -}-  | Done [Arg String] Term+  | Done [Arg ArgName] Term     -- ^ @Done xs b@ stands for the body @b@ where the @xs@ contains hiding     --   and name suggestions for the free variables. This is needed to build     --   lambdas on the right hand side for partial applications which can
src/full/Agda/TypeChecking/CompiledClause/Compile.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.CompiledClause.Compile where  import Data.Monoid@@ -111,7 +112,7 @@     []          -> __IMPOSSIBLE__   where     name (VarP x) = x-    name (DotP _) = "_"+    name (DotP _) = underscore     name ConP{}  = __IMPOSSIBLE__     name LitP{}  = __IMPOSSIBLE__     name ProjP{} = __IMPOSSIBLE__@@ -217,7 +218,7 @@      expand ps b q =       case q of-        ConP c _ qs' -> (ps0 ++ [defaultArg $ ConP c Nothing (genericReplicate m $ defaultArg $ unnamed $ VarP "_")] ++ ps1,+        ConP c _ qs' -> (ps0 ++ [defaultArg $ ConP c Nothing (genericReplicate m $ defaultArg $ unnamed $ VarP underscore)] ++ ps1,                          substBody n' m (Con c (map var [m - 1, m - 2..0])) b)           where m = length qs'         LitP l -> (ps0 ++ [defaultArg $ LitP l] ++ ps1, substBody n' 0 (Lit l) b)@@ -239,7 +240,7 @@ substBody :: Int -> Int -> Term -> ClauseBody -> ClauseBody substBody _ _ _ NoBody = NoBody substBody 0 m v b = case b of-  Bind   b -> foldr (.) id (replicate m (Bind . Abs "_")) $ subst v (absBody $ raise m b)+  Bind   b -> foldr (.) id (replicate m (Bind . Abs underscore)) $ subst v (absBody $ raise m b)   _        -> __IMPOSSIBLE__ substBody n m v b = case b of   Bind b   -> Bind $ fmap (substBody (n - 1) m v) b
src/full/Agda/TypeChecking/CompiledClause/Match.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE CPP, PatternGuards, ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+ module Agda.TypeChecking.CompiledClause.Match where  import Control.Applicative
src/full/Agda/TypeChecking/Constraints.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Constraints where  import Control.Monad.State
src/full/Agda/TypeChecking/Conversion.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.Conversion where @@ -8,9 +11,9 @@ import Control.Monad.State import Control.Monad.Error -import Data.Traversable hiding (mapM, sequence) import Data.List hiding (sort) import qualified Data.List as List+import Data.Traversable hiding (mapM, sequence)  import Agda.Syntax.Abstract.Views (isSet) import Agda.Syntax.Common@@ -292,7 +295,7 @@     equalFun (Pi dom@(Dom info _) b) m n = do         -- name <- freshName_ $ properName $ absName b         name <- freshName_ $ suggest (absName b) "x"-        addCtx name dom $ compareTerm cmp (absBody b) m' n'+        addContext (name, dom) $ compareTerm cmp (absBody b) m' n'       where         (m',n') = raise 1 (m,n) `apply` [Arg info $ var 0] {-@@ -325,7 +328,7 @@           dom <- if dependent                  then Dom i1 <$> blockTypeOnProblem a1 pid                  else return dom1-          addCtx name dom $ compareTel t1 t2 cmp (absBody tel1) (absBody tel2)+          addContext (name, dom) $ compareTel t1 t2 cmp (absBody tel1) (absBody tel2)           stealConstraints pid  {- OLD, before 2013-05-15@@ -597,7 +600,7 @@                        -- then Dom i1 . El a1s <$> blockTermOnProblem (El Inf $ Sort a1s) a1t pid                        else return dom1                 name <- freshName_ (suggest b1 b2)-                addCtx name dom $ compareType cmp (absBody b1) (absBody b2)+                addContext (name, dom) $ compareType cmp (absBody b1) (absBody b2)                 stealConstraints pid                 -- Andreas, 2013-05-15 Now, comparison of codomains is not                 -- blocked any more by getting stuck on domains.@@ -917,21 +920,27 @@ coerceSize :: Term -> Type -> Type -> TCM Term coerceSize v t1 t2 = workOnTypes $ do   let fallback = v <$ leqType t1 t2-      succeed  = return v   caseMaybeM (isSizeType t1) fallback $ \ b1 -> do   caseMaybeM (isSizeType t2) fallback $ \ b2 -> do     case b2 of       -- @t2 = Size@.  We are done!-      BoundedNo -> succeed+      BoundedNo -> return v       -- @t2 = Size< v2@       BoundedLt v2 -> do         sv2 <- sizeView v2         case sv2 of           SizeInf     -> fallback-          OtherSize{} -> fallback  -- TODO: this is not precise+          OtherSize{} -> do+            -- Andreas, 2014-06-16:+            -- Issue 1203: For now, just treat v < v2 as suc v <= v2+            -- TODO: Need proper < comparison+            vinc <- sizeSuc 1 v+            compareSizes CmpLeq vinc v2+            return v           -- @v2 = a2 + 1@: In this case, we can try @v <= a2@           SizeSuc a2 -> do-            ifM (tryConversion $ compareSizes CmpLeq v a2) succeed fallback+            compareSizes CmpLeq v a2+            return v  --------------------------------------------------------------------------- -- * Sorts and levels@@ -943,7 +952,7 @@  compareSort :: Comparison -> Sort -> Sort -> TCM () compareSort CmpEq  = equalSort-compareSort CmpLeq = equalSort+compareSort CmpLeq = leqSort  -- | Check that the first sort is less or equal to the second. leqSort :: Sort -> Sort -> TCM ()@@ -951,6 +960,7 @@   ifM typeInType (return ()) $     catchConstraint (SortCmp CmpLeq s1 s2) $     do	(s1,s2) <- reduce (s1,s2)+        let postpone = addConstraint (SortCmp CmpLeq s1 s2)         reportSDoc "tc.conv.sort" 30 $           sep [ text "leqSort"               , nest 2 $ fsep [ prettyTCM s1 <+> text "=<"@@ -967,8 +977,8 @@              (_       , Inf     )             -> return ()             (Inf     , _       )             -> equalSort s1 s2-            (DLub{}  , _       )             -> equalSort s1 s2-            (_       , DLub{}  )             -> equalSort s1 s2+            (DLub{}  , _       )             -> postpone+            (_       , DLub{}  )             -> postpone     where 	notLeq s1 s2 = typeError $ NotLeqSort s1 s2 @@ -1249,6 +1259,7 @@   ifM typeInType (return ()) $     catchConstraint (SortCmp CmpEq s1 s2) $ do         (s1,s2) <- reduce (s1,s2)+        let postpone = addConstraint (SortCmp CmpEq s1 s2)         reportSDoc "tc.conv.sort" 30 $           sep [ text "equalSort"               , vcat [ nest 2 $ fsep [ prettyTCM s1 <+> text "=="@@ -1268,17 +1279,20 @@             (Inf     , Inf     )             -> return ()             (Inf     , Type (Max as@(_:_)))  -> mapM_ (isInf $ notEq s1 s2) as             (Type (Max as@(_:_)), Inf)       -> mapM_ (isInf $ notEq s1 s2) as+            -- Andreas, 2014-06-27:+            -- @Type (Max [])@ (which is Set0) falls through to error.             (Inf     , _       )             -> notEq s1 s2             (_       , Inf     )             -> notEq s1 s2 +            -- Andreas, 2014-06-27:  Why are there special cases for Set0?             (DLub s1 s2, s0@(Type (Max []))) -> do               equalSort s1 s0               underAbstraction_ s2 $ \s2 -> equalSort s2 s0             (s0@(Type (Max [])), DLub s1 s2) -> do               equalSort s0 s1               underAbstraction_ s2 $ \s2 -> equalSort s0 s2-            (DLub{}  , _       )             -> addConstraint (SortCmp CmpEq s1 s2)-            (_       , DLub{}  )             -> addConstraint (SortCmp CmpEq s1 s2)+            (DLub{}  , _       )             -> postpone+            (_       , DLub{}  )             -> postpone     where 	notEq s1 s2 = typeError $ UnequalSorts s1 s2
src/full/Agda/TypeChecking/Coverage.hs view
@@ -1,16 +1,21 @@-{-# LANGUAGE CPP, PatternGuards, FlexibleContexts, TupleSections #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}  module Agda.TypeChecking.Coverage where  import Control.Monad import Control.Monad.Error-import Control.Applicative+import Control.Applicative hiding (empty)+ import Data.List import qualified Data.Set as Set import Data.Set (Set) import qualified Data.Traversable as Trav  import Agda.Syntax.Position+import qualified Agda.Syntax.Common as Common import Agda.Syntax.Common hiding (Arg,Dom) import qualified Agda.Syntax.Common as C import Agda.Syntax.Internal as I@@ -79,7 +84,7 @@   { scTel    = clauseTel  cl   , scPerm   = clausePerm cl   , scPats   = namedClausePats cl-  , scSubst  = __IMPOSSIBLE__+  , scSubst  = idS  -- Andreas, 2014-07-15  TODO: Is this ok?   , scTarget = clauseType cl   } @@ -175,42 +180,48 @@       reportSLn "tc.cover" 20 $ "blocked by projection pattern"       -- if we want to split projections, but have no target type, we give up       let done = return (SplittingDone (size tel), Set.empty, [ps])-      caseMaybe target done $ \ t -> do-        isR <- addCtxTel tel $ isRecordType $ unArg t-        case isR of-          Just (_r, vs, Record{ recFields = fs }) -> do-            reportSDoc "tc.cover" 20 $ sep-              [ text $ "we are of record type _r = " ++ show _r-              , text   "applied to parameters vs = " <+> (addCtxTel tel $ prettyTCM vs)-              , text $ "and have fields       fs = " ++ show fs-              ]---            es <- patternsToElims perm ps-            fvs <- freeVarsToApply f-            let es = patternsToElims perm ps-            let self  = defaultArg $ Def f (map Apply fvs) `applyE` es-                pargs = vs ++ [self]-            reportSDoc "tc.cover" 20 $ sep-              [ text   "we are              self = " <+> (addCtxTel tel $ prettyTCM $ unArg self)-              ]-            (projs, (trees, useds, psss)) <- mapSnd unzip3 . unzip <$> do-              forM fs $ \ proj -> do-                -- compute the new target-                dType <- defType <$> do getConstInfo $ unArg proj -- WRONG: typeOfConst $ unArg proj-                let -- type of projection instantiated at self-                    target' = Just $ proj $> dType `apply` pargs-                    sc' = sc { scPats   = scPats sc ++ [fmap (Named Nothing . ProjP) proj]-                             , scTarget = target'-                             }-                (unArg proj,) <$> do cover f cs =<< fixTarget sc'-            let -- WRONG: -- n = length ps -- past the last argument, is pos. of proj pat.-                -- n = size tel -- past the last variable, is pos. of proj pat. DURING SPLITTING-                n = permRange perm -- Andreas & James, 2013-11-19 includes the dot patterns!-                -- See test/succeed/CopatternsAndDotPatterns.agda for a case with dot patterns-                -- and copatterns which fails for @n = size tel@ with a broken case tree.-                tree = SplitAt n $ zip projs trees-            return (tree, Set.unions useds, concat psss)-          _ -> done+      caseMaybeM (splitResult f sc) done $ \ (Covering n scs) -> do+        (projs, (trees, useds, psss)) <- mapSnd unzip3 . unzip <$> do+          forM scs $ \ (proj, sc') -> (proj,) <$> do cover f cs =<< fixTarget sc'+          -- OR: mapM (traverseF $ cover f cs <=< fixTarget) scs+        let tree = SplitAt n $ zip projs trees+        return (tree, Set.unions useds, concat psss) +      -- caseMaybe target done $ \ t -> do+      --   isR <- addCtxTel tel $ isRecordType $ unArg t+      --   case isR of+      --     Just (_r, vs, Record{ recFields = fs }) -> do+      --       reportSDoc "tc.cover" 20 $ sep+      --         [ text $ "we are of record type _r = " ++ show _r+      --         , text   "applied to parameters vs = " <+> (addCtxTel tel $ prettyTCM vs)+      --         , text $ "and have fields       fs = " ++ show fs+      --         ]+      --       fvs <- freeVarsToApply f+      --       let es = patternsToElims perm ps+      --       let self  = defaultArg $ Def f (map Apply fvs) `applyE` es+      --           pargs = vs ++ [self]+      --       reportSDoc "tc.cover" 20 $ sep+      --         [ text   "we are              self = " <+> (addCtxTel tel $ prettyTCM $ unArg self)+      --         ]+      --       (projs, (trees, useds, psss)) <- mapSnd unzip3 . unzip <$> do+      --         forM fs $ \ proj -> do+      --           -- compute the new target+      --           dType <- defType <$> do getConstInfo $ unArg proj -- WRONG: typeOfConst $ unArg proj+      --           let -- type of projection instantiated at self+      --               target' = Just $ proj $> dType `apply` pargs+      --               sc' = sc { scPats   = scPats sc ++ [fmap (Named Nothing . ProjP) proj]+      --                        , scTarget = target'+      --                        }+      --           (unArg proj,) <$> do cover f cs =<< fixTarget sc'+      --       let -- WRONG: -- n = length ps -- past the last argument, is pos. of proj pat.+      --           -- n = size tel -- past the last variable, is pos. of proj pat. DURING SPLITTING+      --           n = permRange perm -- Andreas & James, 2013-11-19 includes the dot patterns!+      --           -- See test/succeed/CopatternsAndDotPatterns.agda for a case with dot patterns+      --           -- and copatterns which fails for @n = size tel@ with a broken case tree.+      --           tree = SplitAt n $ zip projs trees+      --       return (tree, Set.unions useds, concat psss)+      --     _ -> done+     -- case: split on variable     Block bs -> do       reportSLn "tc.cover.strategy" 20 $ "blocking vars = " ++ show bs@@ -238,7 +249,7 @@           return (tree, Set.unions useds, concat psss)  splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars-splitStrategy bs tel = return $ updateLast (mapSnd (const Nothing)) xs+splitStrategy bs tel = return $ updateLast clearBlockingVarCons xs   -- Make sure we do not insists on precomputed coverage when   -- we make our last try to split.   -- Otherwise, we will not get a nice error message.@@ -296,7 +307,7 @@       text "telescope (after substitution): " <+> prettyTCM tel     let n      = size tel         lgamma = telToList tel-        xs     = for lgamma $ (namedVarP "_" <$) . argFromDom+        xs     = for lgamma $ \ (Common.Dom ai (x, _)) -> Common.Arg ai $ namedVarP "_"     if (n == 0) then return sc { scTarget = Just $ a $> b }      else return $ SClause       { scTel    = telFromList $ telToList (scTel sc) ++ lgamma@@ -322,7 +333,7 @@ --   @dtype == d pars ixs@ computeNeighbourhood   :: Telescope                  -- ^ Telescope before split point.-  -> String                     -- ^ Name of pattern variable at split point.+  -> PatVarName                 -- ^ Name of pattern variable at split point.   -> Telescope                  -- ^ Telescope after split point.   -> Permutation                -- ^   -> QName                      -- ^ Name of datatype to split at.@@ -498,16 +509,26 @@         ]  -- | Entry point from @Interaction.MakeCase@.---   @Abs@ is for absurd clause.-splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))-splitClauseWithAbs c x = split' Inductive (clauseToSplitClause c) (x, Nothing)+splitClauseWithAbsurd :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))+splitClauseWithAbsurd c x = split' Inductive (clauseToSplitClause c) (BlockingVar x Nothing)  -- | Entry point from @TypeChecking.Empty@ and @Interaction.BasicOps@. splitLast :: Induction -> Telescope -> [I.NamedArg Pattern] -> TCM (Either SplitError Covering)-splitLast ind tel ps = split ind sc (0, Nothing)+splitLast ind tel ps = split ind sc (BlockingVar 0 Nothing)   where sc = SClause tel (idP $ size tel) ps __IMPOSSIBLE__ Nothing --- | @split _ Δ π ps x@. FIXME: Δ ⊢ ps, x ∈ Δ (deBruijn index)+-- | @split ind splitClause x = return res@+--   splits @splitClause@ at pattern var @x@ (de Bruijn index).+--+--   Possible results @res@ are:+--+--   1. @Left err@:+--      Splitting failed.+--+--   2. @Right covering@:+--      A covering set of split clauses, one for each valid constructor.+--      This could be the empty set (denoting an absurd clause).+ split :: Induction          -- ^ Coinductive constructors are allowed if this argument is          -- 'CoInductive'.@@ -515,22 +536,14 @@       -> BlockingVar       -> TCM (Either SplitError Covering) split ind sc x = fmap (blendInAbsurdClause (splitDbIndexToLevel sc x)) <$>-   split' ind sc x-{- OLD-split ind sc@SClause{ scTel = tel, scPerm = perm, scPats = ps } x =-  r <- split' ind sc x-  return $ case r of-    Left err        -> Left err-    Right (Left _)  -> Right $ Covering (dbIndexToLevel tel perm $ fst x) []-    Right (Right c) -> Right c--}--blendInAbsurdClause :: Nat -> Either SplitClause Covering -> Covering-blendInAbsurdClause n = either (const $ Covering n []) id+    split' ind sc x+  where+    blendInAbsurdClause :: Nat -> Either SplitClause Covering -> Covering+    blendInAbsurdClause n = either (const $ Covering n []) id -splitDbIndexToLevel :: SplitClause -> BlockingVar -> Nat-splitDbIndexToLevel sc@SClause{ scTel = tel, scPerm = perm } x =-  dbIndexToLevel tel perm $ fst x+    splitDbIndexToLevel :: SplitClause -> BlockingVar -> Nat+    splitDbIndexToLevel sc@SClause{ scTel = tel, scPerm = perm } x =+      dbIndexToLevel tel perm $ blockingVarNo x  -- | Convert a de Bruijn index relative to a telescope to a de Buijn level. --   The result should be the argument (counted from left, starting with 0)@@ -539,13 +552,27 @@   where n = if k < 0 then __IMPOSSIBLE__ else permute perm [0..] !! k         k = size tel - x - 1 +-- | @split' ind splitClause x = return res@+--   splits @splitClause@ at pattern var @x@ (de Bruijn index).+--+--   Possible results @res@ are:+--+--   1. @Left err@:+--      Splitting failed.+--+--   2. @Right (Left splitClause')@:+--      Absurd clause (type of @x@ has 0 valid constructors).+--+--   3. @Right (Right covering)@:+--      A covering set of split clauses, one for each valid constructor.+ split' :: Induction           -- ^ Coinductive constructors are allowed if this argument is           -- 'CoInductive'.        -> SplitClause        -> BlockingVar        -> TCM (Either SplitError (Either SplitClause Covering))-split' ind sc@(SClause tel perm ps _ target) (x, mcons) = liftTCM $ runExceptionT $ do+split' ind sc@(SClause tel perm ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do    debugInit tel perm x ps @@ -639,9 +666,57 @@      debugHoleAndType delta1 delta2 s hps t =       liftTCM $ reportSDoc "tc.cover.top" 10 $ nest 2 $ vcat $-        [ text "p      =" <+> text s+        [ text "p      =" <+> text (patVarNameToString s)         , text "hps    =" <+> text (show hps)         , text "delta1 =" <+> prettyTCM delta1         , text "delta2 =" <+> inContextOfDelta2 (prettyTCM delta2)         , text "t      =" <+> inContextOfT (prettyTCM t)         ]++-- | @splitResult f sc = return res@+--+--   If the target type of @sc@ is a record type, a covering set of+--   split clauses is returned (@sc@ extended by all valid projection patterns),+--   otherwise @res == Nothing@.+--   Note that the empty set of split clauses is returned if the record has no fields.+splitResult :: QName -> SplitClause -> TCM (Maybe Covering)+splitResult f sc@(SClause tel perm ps _ target) = do+  reportSDoc "tc.cover.split" 10 $ vcat+    [ text "splitting result:"+    , nest 2 $ text "f      =" <+> text (show f)+    , nest 2 $ text "target =" <+> (addContext tel $ maybe empty prettyTCM target)+    ]+  -- if we want to split projections, but have no target type, we give up+  let done = return Nothing+  caseMaybe target done $ \ t -> do+    isR <- addCtxTel tel $ isRecordType $ unArg t+    case isR of+      Just (_r, vs, Record{ recFields = fs }) -> do+        reportSDoc "tc.cover" 20 $ sep+          [ text $ "we are of record type _r = " ++ show _r+          , text   "applied to parameters vs = " <+> (addCtxTel tel $ prettyTCM vs)+          , text $ "and have fields       fs = " ++ show fs+          ]+        fvs <- freeVarsToApply f+        let es = patternsToElims perm ps+        let self  = defaultArg $ Def f (map Apply fvs) `applyE` es+            pargs = vs ++ [self]+        reportSDoc "tc.cover" 20 $ sep+          [ text   "we are              self = " <+> (addCtxTel tel $ prettyTCM $ unArg self)+          ]+        let -- WRONG: -- n = length ps -- past the last argument, is pos. of proj pat.+            -- n = size tel -- past the last variable, is pos. of proj pat. DURING SPLITTING+            n = permRange perm -- Andreas & James, 2013-11-19 includes the dot patterns!+            -- See test/succeed/CopatternsAndDotPatterns.agda for a case with dot patterns+            -- and copatterns which fails for @n = size tel@ with a broken case tree.+        Just . Covering n <$> do+          forM fs $ \ proj -> do+            -- compute the new target+            dType <- defType <$> do getConstInfo $ unArg proj -- WRONG: typeOfConst $ unArg proj+            let -- type of projection instantiated at self+                target' = Just $ proj $> dType `apply` pargs+                sc' = sc { scPats   = scPats sc ++ [fmap (Named Nothing . ProjP) proj]+                         , scTarget = target'+                         }+            return (unArg proj, sc')+      _ -> done
src/full/Agda/TypeChecking/Coverage/Match.hs view
@@ -1,10 +1,13 @@-{-# LANGUAGE CPP, PatternGuards, DeriveFunctor #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE PatternGuards #-}  module Agda.TypeChecking.Coverage.Match where  import Control.Applicative import Control.Monad.State +import qualified Data.List as List import Data.Maybe (mapMaybe) import Data.Monoid import Data.Traversable (traverse)@@ -66,7 +69,7 @@ --   against a clause. In particular we want to keep track of which variables --   are blocking a match. data MPat-  = VarMP Nat+  = VarMP Nat    -- ^ De Bruijn index (usually, rightmost variable in patterns is 0).   | ConMP ConHead [Arg MPat]   | LitMP Literal   | WildMP       -- ^ For dot patterns that cannot be turned into patterns.@@ -99,22 +102,37 @@   | BlockP               -- ^ Could match if split on possible projections is performed.   deriving (Functor) --- | @Nothing@ means there is an overlapping match for this variable.---   @Just cons@ means that it is an non-overlapping match and---   @cons@ are the encountered constructors.-type BlockingVar  = (Nat, (Maybe [ConHead]))+-- | Variable blocking a match.+data BlockingVar  = BlockingVar+  { blockingVarNo   :: Nat+    -- ^ De Bruijn index of variable blocking the match.+  , blockingVarCons :: Maybe [ConHead]+    -- ^ @Nothing@ means there is an overlapping match for this variable.+    --   This happens if one clause has a constructor pattern at this position,+    --   and another a variable.  It is also used for "just variable".+    --+    --   @Just cons@ means that it is an non-overlapping match and+    --   @cons@ are the encountered constructors.+  } deriving (Show) type BlockingVars = [BlockingVar] +mapBlockingVarCons :: (Maybe [ConHead] -> Maybe [ConHead]) -> BlockingVar -> BlockingVar+mapBlockingVarCons f b = b { blockingVarCons = f (blockingVarCons b) }++clearBlockingVarCons :: BlockingVar -> BlockingVar+clearBlockingVarCons = mapBlockingVarCons $ const Nothing+ overlapping :: BlockingVars -> BlockingVars-overlapping = map $ \ (x, _) -> (x, Nothing)+overlapping = map clearBlockingVarCons  -- | Left dominant merge of blocking vars. zipBlockingVars :: BlockingVars -> BlockingVars -> BlockingVars zipBlockingVars xs ys = map upd xs   where-    upd (x, Just cons) | Just (Just cons') <- lookup x ys =-     (x, Just $ cons ++ cons')-    upd (x, _) = (x, Nothing)+    upd (BlockingVar x (Just cons))+      | Just (BlockingVar _ (Just cons')) <- List.find ((x ==) . blockingVarNo) ys+                          = BlockingVar x (Just $ cons ++ cons')+    upd (BlockingVar x _) = BlockingVar x Nothing  -- | @choice m m'@ combines the match results @m@ of a function clause --   with the (already combined) match results $m'$ of the later clauses.@@ -223,7 +241,7 @@ matchPat _    (ProjP d) _ = __IMPOSSIBLE__ -- matchPat mlit (ConP c (Just _) ps) q | recordPattern ps = Yes ()  -- Andreas, 2012-07-25 record patterns always match! matchPat mlit (ConP c _ ps) q = case q of-  VarMP x -> Block [(x, Just [c])]+  VarMP x -> Block [BlockingVar x (Just [c])]   WildMP{} -> No -- Andreas, 2013-05-15 this was "Yes()" triggering issue 849   ConMP c' qs     | c == c'   -> matchPats mlit (map (fmap namedThing) ps) qs
src/full/Agda/TypeChecking/DisplayForm.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.DisplayForm where
src/full/Agda/TypeChecking/DropArgs.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}+ module Agda.TypeChecking.DropArgs where  import Agda.Syntax.Internal
src/full/Agda/TypeChecking/Empty.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP #-}+-- {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Empty where  import Control.Applicative@@ -34,7 +35,7 @@     -- from the current context xs:ts, create a pattern list     -- xs _ : ts t and try to split on _ (the last variable)       tel0 <- getContextTelescope-      let gamma = telToList tel0 ++ [domFromArg $ defaultArg ("_", t)]+      let gamma = telToList tel0 ++ [domFromArg $ defaultArg (underscore, t)]           ps    = [ Arg info $ namedVarP x | Dom info (x, _) <- gamma ]           tel   = telFromList gamma
src/full/Agda/TypeChecking/Errors.hs view
@@ -1,5 +1,8 @@-{-# LANGUAGE CPP, TupleSections,-      FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+ module Agda.TypeChecking.Errors     ( prettyError     , PrettyTCM(..)@@ -152,6 +155,7 @@     GenericDocError{}                        -> "GenericDocError"     IFSNoCandidateInScope{}                  -> "IFSNoCandidateInScope"     IlltypedPattern{}                        -> "IlltypedPattern"+    IllformedProjectionPattern{}             -> "IllformedProjectionPattern"     CannotEliminateWithPattern{}             -> "CannotEliminateWithPattern"     IllegalLetInTelescope{}                  -> "IllegalLetInTelescope"     IncompletePatternMatching{}              -> "IncompletePatternMatching"@@ -340,6 +344,8 @@               pwords "Failed to infer the value of dotted pattern"             IlltypedPattern p a -> fsep $               pwords "Type mismatch"+            IllformedProjectionPattern p -> fsep $+              pwords "Ill-formed projection pattern " ++ [prettyA p]             CannotEliminateWithPattern p a -> do               let isProj = isJust (isProjP p)               fsep $@@ -353,7 +359,7 @@               pwords "Left hand side gives too many arguments to a function of type" ++ [prettyTCM a]             WrongNumberOfConstructorArguments c expect given -> fsep $               pwords "The constructor" ++ [prettyTCM c] ++ pwords "expects" ++-              [text (show expect)] ++ pwords "arguments, but has been given" ++ [text (show given)]+              [text (show expect)] ++ pwords "arguments (including hidden ones), but has been given" ++ [text (show given)] ++ pwords "(including hidden ones)"             CantResolveOverloadedConstructorsTargetingSameDatatype d cs -> fsep $               pwords ("Can't resolve overloaded constructors targeting the same datatype (" ++ show d ++ "):") ++ map (text . show) cs             DoesNotConstructAnElementOf c t -> fsep $@@ -934,7 +940,7 @@             info = A.ModuleInfo noRange noRange Nothing Nothing Nothing  	where-            hPretty :: I.Arg (Named RString Expr) -> TCM Doc+            hPretty :: I.Arg (Named_ Expr) -> TCM Doc             hPretty a = do                 info <- reify $ argInfo a                 pretty =<< (abstractToConcreteCtx (hiddenArgumentCtx (getHiding a))
src/full/Agda/TypeChecking/EtaContract.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards, FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PatternGuards #-}  -- | Compute eta short normal forms. module Agda.TypeChecking.EtaContract where
src/full/Agda/TypeChecking/Forcing.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Forcing where  import Control.Applicative
src/full/Agda/TypeChecking/Free.hs view
@@ -1,5 +1,6 @@ -- {-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | Computing the free variables of a term. module Agda.TypeChecking.Free
src/full/Agda/TypeChecking/Implicit.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}  {-| Functions for inserting implicit arguments at the right places. -}@@ -33,7 +34,7 @@ -- | @implicitNamedArgs n expand t@ generates up to @n@ named implicit arguments --   metas (unbounded if @n<0@), as long as @t@ is a function type --   and @expand@ holds on the hiding and name info of its domain.-implicitNamedArgs :: Int -> (Hiding -> String -> Bool) -> Type -> TCM (NamedArgs, Type)+implicitNamedArgs :: Int -> (Hiding -> ArgName -> Bool) -> Type -> TCM (NamedArgs, Type) implicitNamedArgs 0 expand t0 = return ([], t0) implicitNamedArgs n expand t0 = do     t0' <- reduce t0@@ -42,7 +43,7 @@           when (getHiding info == Instance) $ reportSLn "tc.term.args.ifs" 15 $             "inserting instance meta for type " ++ show a           v  <- applyRelevanceToContext (getRelevance info) $-                newMeta (getHiding info) x a+                newMeta (getHiding info) (argNameToString x) a           let narg = Arg info (Named (Just $ unranged x) v)           mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)       _ -> return ([], t0')@@ -76,7 +77,7 @@ data ImplicitInsertion       = ImpInsert [Hiding]	  -- ^ this many implicits have to be inserted       | BadImplicits	  -- ^ hidden argument where there should have been a non-hidden arg-      | NoSuchName String -- ^ bad named argument+      | NoSuchName ArgName -- ^ bad named argument       | NoInsertNeeded   deriving (Show) @@ -85,7 +86,7 @@ impInsert hs = ImpInsert hs  -- | The list should be non-empty.-insertImplicit :: A.NamedArg e -> [I.Arg String] -> ImplicitInsertion+insertImplicit :: A.NamedArg e -> [I.Arg ArgName] -> ImplicitInsertion insertImplicit _ [] = __IMPOSSIBLE__ insertImplicit a ts | notHidden a = impInsert $ nofHidden ts   where@@ -100,6 +101,7 @@     upto h (NotHidden:_) = Nothing     upto h (h':_) | h == h' = Just []     upto h (h':hs) = (h':) <$> upto h hs+    find :: [Hiding] -> ArgName -> Hiding -> [I.Arg ArgName] -> ImplicitInsertion     find _ x _ (a@(Arg{}) : _) | notHidden a = NoSuchName x     find hs x hidingx (a@(Arg _ y) : ts)       | x == y && hidingx == getHiding a = impInsert $ reverse hs
src/full/Agda/TypeChecking/Level.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Level where  import Control.Monad.Error
src/full/Agda/TypeChecking/MetaVars.hs view
@@ -1,5 +1,10 @@-{-# LANGUAGE CPP, TupleSections, PatternGuards, RelaxedPolyRec, GeneralizedNewtypeDeriving,-      FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE RelaxedPolyRec #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.MetaVars where
src/full/Agda/TypeChecking/MetaVars/Occurs.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.MetaVars.Occurs where @@ -207,7 +209,7 @@     where       occurs' ctx v = do       reportSDoc "tc.meta.occurs" 45 $-        text ("occursCheck (" ++ show ctx ++ ") of ") <+> prettyTCM v+        text ("occursCheck " ++ show m ++ " (" ++ show ctx ++ ") of ") <+> prettyTCM v       reportSDoc "tc.meta.occurs" 70 $         nest 2 $ text $ show v       case v of@@ -352,9 +354,9 @@       MetaLevel m' args -> do         MetaV m' args <- ignoreSharing <$> occurs red ctx m xs (MetaV m' args)         return $ MetaLevel m' args-      NeutralLevel v   -> NeutralLevel   <$> occurs red ctx m xs v-      BlockedLevel m v -> BlockedLevel m <$> occurs red Flex m xs v-      UnreducedLevel v -> UnreducedLevel <$> occurs red ctx m xs v+      NeutralLevel v    -> NeutralLevel    <$> occurs red ctx m xs v+      BlockedLevel m' v -> BlockedLevel m' <$> occurs red Flex m xs v+      UnreducedLevel v  -> UnreducedLevel  <$> occurs red ctx m xs v    metaOccurs m l = do     l <- instantiate l@@ -538,7 +540,8 @@   | not (or kills) = return NothingToPrune  -- nothing to kill killArgs kills m = do   mv <- lookupMeta m-  if mvFrozen mv == Frozen then return PrunedNothing else do+  allowAssign <- asks envAssignMetas+  if mvFrozen mv == Frozen || not allowAssign then return PrunedNothing else do {- Andreas 2011-04-26, allow pruning in MetaS   case mvJudgement mv of     IsSort _    -> return False@@ -580,7 +583,7 @@ --   Invariant: @k'i == True@ iff @ki == True@ and pruning the @i@th argument from --   type @b@ is possible without creating unbound variables. --   @t'@ is type @t@ after pruning all @k'i==True@.-killedType :: [(I.Dom (String, Type), Bool)] -> Type -> ([I.Arg Bool], Type)+killedType :: [(I.Dom (ArgName, Type), Bool)] -> Type -> ([I.Arg Bool], Type) killedType [] b = ([], b) killedType ((arg@(Dom info _), kill) : kills) b   | dontKill  = (Arg info False : args, mkPi arg b') -- OLD: telePi (telFromList [arg]) b')
src/full/Agda/TypeChecking/Monad/Base.hs view
@@ -1,9 +1,19 @@-{-# LANGUAGE CPP, NamedFieldPuns, ScopedTypeVariables,-             ExistentialQuantification, FlexibleContexts, Rank2Types,-             TypeSynonymInstances, MultiParamTypeClasses, FlexibleInstances,-             UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving,-             DeriveFunctor, DeriveFoldable, DeriveTraversable-  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}+ module Agda.TypeChecking.Monad.Base where  import Control.Arrow ((***), first, second)@@ -773,6 +783,7 @@             , funInv            :: FunctionInverse             , funMutual         :: [QName]               -- ^ Mutually recursive functions, @data@s and @record@s.+              --   Does not include this function.             , funAbstr          :: IsAbstract             , funDelayed        :: Delayed               -- ^ Are the clauses of this definition delayed?@@ -806,7 +817,7 @@             , dataClause         :: (Maybe Clause) -- ^ This might be in an instantiated module.             , dataCons           :: [QName]        -- ^ Constructor names.             , dataSort           :: Sort-            , dataMutual         :: [QName]        -- ^ Mutually recursive functions, @data@s and @record@s.+            , dataMutual         :: [QName]        -- ^ Mutually recursive functions, @data@s and @record@s.  Does not include this data type.             , dataAbstr          :: IsAbstract             } 	  | Record@@ -819,7 +830,7 @@             , recTel            :: Telescope            -- ^ The record field telescope. (Includes record parameters.)                                                         --   Note: @TelV recTel _ == telView' recConType@.                                                         --   Thus, @recTel@ is redundant.-            , recMutual         :: [QName]              -- ^ Mutually recursive functions, @data@s and @record@s.+            , recMutual         :: [QName]              -- ^ Mutually recursive functions, @data@s and @record@s.  Does not include this record.             , recEtaEquality    :: Bool                 -- ^ Eta-expand at this record type.  @False@ for unguarded recursive records and coinductive records.             , recInduction      :: Induction            -- ^ 'Inductive' or 'Coinductive'?  Matters only for recursive records.             , recRecursive      :: Bool                 -- ^ Recursive record.  Implies @recEtaEquality = False@.  Projections are not size-preserving.@@ -1417,6 +1428,7 @@           -- ^ The term does not correspond to an inductive data type. 	| UninstantiatedDotPattern A.Expr 	| IlltypedPattern A.Pattern Type+	| IllformedProjectionPattern A.Pattern 	| CannotEliminateWithPattern (A.NamedArg A.Pattern) Type 	| TooManyArgumentsInLHS Type 	| WrongNumberOfConstructorArguments QName Nat Nat@@ -1827,5 +1839,5 @@  -- | Check whether we have an definition from an absurd lambda. isAbsurdLambdaName :: QName -> Bool-isAbsurdLambdaName (QName _ Name{nameConcrete = C.Name _ [C.Id ".absurdlambda"]}) = True+isAbsurdLambdaName (QName _ x) | show x == absurdLambdaName = True isAbsurdLambdaName _ = False
src/full/Agda/TypeChecking/Monad/Constraints.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Monad.Constraints where  import Control.Arrow ((&&&))
src/full/Agda/TypeChecking/Monad/Context.hs view
@@ -162,7 +162,7 @@     x <- freshName_ $ realName $ absName a     addCtx x t $ k $ absBody a   where-    realName s = if isNoName s then "x" else s+    realName s = if isNoName s then "x" else argNameToString s  -- | Go under an abstract without worrying about the type to add to the context. {-# SPECIALIZE underAbstraction_ :: Subst a => Abs a -> (a -> TCM b) -> TCM b #-}@@ -210,7 +210,7 @@ -- | Get the current context as a 'Telescope'. {-# SPECIALIZE getContextTelescope :: TCM Telescope #-} getContextTelescope :: MonadTCM tcm => tcm Telescope-getContextTelescope = telFromList' show . reverse <$> getContext+getContextTelescope = telFromList' nameToArgName . reverse <$> getContext  -- | Check if we are in a compatible context, i.e. an extension of the given context. {-# SPECIALIZE getContextId :: TCM [CtxId] #-}
src/full/Agda/TypeChecking/Monad/MetaVars.hs view
@@ -1,5 +1,7 @@-{-# LANGUAGE CPP, TupleSections,-  FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.Monad.MetaVars where
src/full/Agda/TypeChecking/Monad/Options.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}  module Agda.TypeChecking.Monad.Options where
src/full/Agda/TypeChecking/Monad/Sharing.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Monad.Sharing where  import Control.Monad.Reader
src/full/Agda/TypeChecking/Monad/Signature.hs view
@@ -1,13 +1,18 @@-{-# LANGUAGE CPP, PatternGuards, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+ module Agda.TypeChecking.Monad.Signature where  import Control.Applicative import Control.Monad.State import Control.Monad.Reader++import Data.List import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe-import Data.List  import Agda.Syntax.Abstract.Name import Agda.Syntax.Common
src/full/Agda/TypeChecking/Monad/SizedTypes.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, TupleSections, DeriveFunctor #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE TupleSections #-}  -- | Stuff for sized types that does not require modules --   'Agda.TypeChecking.Reduce' or 'Agda.TypeChecking.Constraints'
src/full/Agda/TypeChecking/Patterns/Abstract.hs view
@@ -1,5 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, ScopedTypeVariables,-  TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | Tools to manipulate patterns in abstract syntax --   in the TCM (type checking monad).
src/full/Agda/TypeChecking/Patterns/Match.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, ScopedTypeVariables, DeriveFunctor #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Agda.TypeChecking.Patterns.Match where
src/full/Agda/TypeChecking/Polarity.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}+ module Agda.TypeChecking.Polarity where  import Control.Applicative
src/full/Agda/TypeChecking/Positivity.hs view
@@ -1,5 +1,8 @@-{-# LANGUAGE CPP, FlexibleInstances, FlexibleContexts,-             UndecidableInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}  -- | Check that a datatype is strictly positive. module Agda.TypeChecking.Positivity where@@ -13,7 +16,7 @@ import Data.Map (Map) import qualified Data.Map as Map import Data.List as List-import Data.Maybe (mapMaybe)+import Data.Maybe (mapMaybe, fromMaybe)  import Agda.Syntax.Position import Agda.Syntax.Common@@ -93,15 +96,15 @@           setCurrentRange (getRange q) $ typeError $ GenericError (show err)        -- if we find an unguarded record, mark it as such-      (\ just noth -> maybe noth just (mhead [ how | Edge o how <- loops, o <= StrictPos ]))-        (\ how -> do+      case mhead [ how | Edge o how <- loops, o <= StrictPos ] of+        Just how -> do           reportSDoc "tc.pos.record" 5 $ sep             [ prettyTCM q <+> text "is not guarded, because it occurs"             , prettyTCM how             ]-          unguardedRecord q) $+          unguardedRecord q         -- otherwise, if the record is recursive, mark it as well-        forM_ (take 1 [ how | Edge GuardPos how <- loops ]) $ \ how -> do+        Nothing -> forM_ (take 1 [ how | Edge GuardPos how <- loops ]) $ \ how -> do           reportSDoc "tc.pos.record" 5 $ sep             [ prettyTCM q <+> text "is recursive, because it occurs"             , prettyTCM how@@ -129,7 +132,7 @@       let nArgs = maximum $ n :                     [ i + 1 | (ArgNode q1 i) <- Set.toList $ Graph.nodes g                     , q1 == q ]-          findOcc i = maybe Unused id $ Graph.lookup (ArgNode q i) (DefNode q) g+          findOcc i = fromMaybe Unused $ Graph.lookup (ArgNode q i) (DefNode q) g           args = map findOcc [0..nArgs - 1]       reportSDoc "tc.pos.args" 10 $ sep         [ text "args of" <+> prettyTCM q <+> text "="@@ -509,7 +512,7 @@ etaExpandClause :: Nat -> Clause -> Clause etaExpandClause n c@Clause{ namedClausePats = ps, clauseBody = b }   | m <= 0    = c-  | otherwise = c { namedClausePats = ps ++ genericReplicate m (defaultArg $ unnamed $ VarP "_")+  | otherwise = c { namedClausePats = ps ++ genericReplicate m (defaultArg $ unnamed $ VarP underscore)                   , clauseBody      = liftBody m b                   , clauseTel       = __IMPOSSIBLE__                   , clausePerm      = __IMPOSSIBLE__@@ -518,7 +521,7 @@     m = n - genericLength ps      bind 0 = id-    bind n = Bind . Abs "_" . bind (n - 1)+    bind n = Bind . Abs underscore . bind (n - 1)      vars = map (defaultArg . var) $ downFrom m --    vars = reverse [ defaultArg $ var i | i <- [0..m - 1] ]@@ -549,6 +552,7 @@   prettyTCM Mixed     = text "-[*]->"   prettyTCM Unused    = text "-[ ]->" +-- | Pairing something with a node (for printing only). data WithNode n a = WithNode n a  instance PrettyTCM n => PrettyTCM (WithNode n Edge) where@@ -566,6 +570,7 @@         , nest 2 $ vcat $ map (prettyTCM . uncurry WithNode) $ Map.assocs es         ] +-- | Edge labels for the positivity graph. data Edge = Edge Occurrence OccursWhere   deriving (Show)
src/full/Agda/TypeChecking/Pretty.hs view
@@ -1,6 +1,9 @@-{-# LANGUAGE CPP, ScopedTypeVariables,-  TypeSynonymInstances, FlexibleInstances,-  UndecidableInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}+ module Agda.TypeChecking.Pretty where  import Control.Applicative hiding (empty)@@ -115,7 +118,7 @@       walk (Body v) = (,) [] <$> prettyTCM v       walk (Bind b) = do         (bs, v) <- underAbstraction_ b walk-        return (text (absName b) : bs, v)+        return (text (argNameToString $ absName b) : bs, v)  instance (PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) where   prettyTCM (HasType a t) = prettyTCM a <+> text ":" <+> prettyTCM t@@ -130,7 +133,7 @@   prettyTCM (Blocked x a) = text "[" <+> prettyTCM a <+> text "]" <> text (show x)   prettyTCM (NotBlocked x) = prettyTCM x -instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Named RString a) where+instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Named_ a) where     prettyTCM x = prettyA =<< reify x  instance (Reify a e, ToConcrete e c, P.Pretty c) => PrettyTCM (Arg a) where@@ -280,7 +283,7 @@ instance PrettyTCM Pattern where   prettyTCM = showPat     where-      showPat (VarP x)                  = text x+      showPat (VarP x)                  = text $ patVarNameToString x       showPat (DotP t)                  = text $ ".(" ++ show t ++ ")"       showPat (ConP c Nothing ps)       = parens $         prettyTCM c <+> fsep (map (showPat . namedArg) ps)
src/full/Agda/TypeChecking/Primitive.hs view
@@ -1,7 +1,9 @@-{-# LANGUAGE CPP, FlexibleInstances, UndecidableInstances,-             GeneralizedNewtypeDeriving, ScopedTypeVariables,-             TypeSynonymInstances, FlexibleInstances-  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}  {-| Primitive functions, such as addition on builtin integers. -}@@ -9,9 +11,10 @@  import Control.Monad import Control.Applicative++import Data.Char import Data.Map (Map) import qualified Data.Map as Map-import Data.Char  import Agda.Interaction.Options @@ -235,7 +238,7 @@ 	YesReduction _ y -> k y  redReturn :: a -> ReduceM (Reduced a' a)-redReturn = return . YesReduction NoSimplification+redReturn = return . YesReduction YesSimplification  fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) fromReducedTerm f = return $ \t -> do@@ -449,10 +452,10 @@ gpi :: I.ArgInfo -> String -> TCM Type -> TCM Type -> TCM Type gpi info name a b = do   a <- a-  x <- freshName_ name-  b <- addCtx x (Dom info a) b-  return $ El (getSort a `dLub` Abs name (getSort b))-              (Pi (Dom info a) (Abs name b))+  b <- addContext (name, Dom info a) b+  let y = stringToArgName name+  return $ El (getSort a `dLub` Abs y (getSort b))+              (Pi (Dom info a) (Abs y b))  hPi, nPi :: String -> TCM Type -> TCM Type -> TCM Type hPi = gpi $ setHiding Hidden $ defaultArgInfo
src/full/Agda/TypeChecking/ProjectionLike.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TypeSynonymInstances #-}+ module Agda.TypeChecking.ProjectionLike where  import Control.Monad
src/full/Agda/TypeChecking/Quote.hs view
@@ -1,9 +1,11 @@ {-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.Quote where  import Control.Applicative+ import Data.Maybe (fromMaybe)  import Agda.Syntax.Position@@ -18,6 +20,8 @@ import Agda.TypeChecking.Pretty import Agda.TypeChecking.Substitute +import Agda.Utils.Monad+ #include "../undefined.h" import Agda.Utils.Impossible @@ -67,7 +71,7 @@       quoteSortLevelTerm (Max [])              = setLit @@ Lit (LitInt noRange 0)       quoteSortLevelTerm (Max [ClosedLevel n]) = setLit @@ Lit (LitInt noRange n)       quoteSortLevelTerm (Max [Plus 0 (NeutralLevel v)]) = set @@ quote v-      quoteSortLevelTerm _                     = unsupported+      quoteSortLevelTerm _                     = unsupportedSort       quoteSort (Type t)    = quoteSortLevelTerm t       quoteSort Prop        = unsupportedSort       quoteSort Inf         = unsupportedSort@@ -146,8 +150,7 @@  choice :: Monad m => [(m Bool, m a)] -> m a -> m a choice [] dflt = dflt-choice ((mb, mx) : mxs) dflt = do b <- mb-                                  if b then mx else choice mxs dflt+choice ((mb, mx) : mxs) dflt = ifM mb mx $ choice mxs dflt  instance Unquote I.ArgInfo where   unquote t = do@@ -233,8 +236,8 @@   unquote t = getConHead =<< unquote t  instance Unquote a => Unquote (Abs a) where-  unquote t = do x <- freshNoName_-                 Abs (show x) <$> unquote t+  unquote t = do x <- freshNoName_ -- Andreas, 2014-07-11 This is pointless, as it does NOT generate a name suggestion.+                 Abs (nameToArgName x) <$> unquote t  instance Unquote Sort where   unquote t = do
src/full/Agda/TypeChecking/RecordPatterns.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, TupleSections, FlexibleInstances, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}  -- | Code which replaces pattern matching on record constructors with -- uses of projection functions.@@ -227,7 +231,7 @@           let (xs0,xs1,xs2)     = cutSublist i n xs               names | null xs1  = ["r"]                     | otherwise = map unArg xs1-              x                 = defaultArg $ foldr1 (++) names+              x                 = defaultArg $ foldr1 appendArgNames names               xs'               = xs0 ++ x : xs2               us                = map (\ p -> Var 0 [Proj p]) (reverse projs) --              us                = map (\ p -> Def p [defaultArg $ var 0]) (reverse projs)@@ -568,7 +572,7 @@ -- patterns, should be removed, and a new variable, with the name @x@, -- inserted instead. The type of the new variable is @t@. -type Changes = [Either Pattern (Kind -> Nat, String, I.Dom Type)]+type Changes = [Either Pattern (Kind -> Nat, ArgName, I.Dom Type)]  -- | Record pattern trees. @@ -706,10 +710,10 @@   :: Changes      -- ^ Explanation of how the telescope should be changed. Types      -- should be in the context of the old telescope.-  -> [(String, I.Dom Type)]+  -> [(ArgName, I.Dom Type)]      -- ^ Old telescope, flattened, in textual left-to-right      -- order.-  -> [Maybe (String, I.Dom Type)]+  -> [Maybe (ArgName, I.Dom Type)]      -- ^ New telescope, flattened, in textual left-to-right order.      -- 'Nothing' is used to indicate the locations of dot patterns. translateTel (Left (DotP{}) : rest)   tel = Nothing : translateTel rest tel
src/full/Agda/TypeChecking/Records.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, TupleSections, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}  module Agda.TypeChecking.Records where @@ -130,12 +132,20 @@ --   Succeeds only if type is not blocked by a meta var. --   If yes, return its name, parameters, and definition. isRecordType :: Type -> TCM (Maybe (QName, Args, Defn))-isRecordType t = ifBlockedType t (\ _ _ -> return Nothing) $ \ t -> do+isRecordType t = either (const Nothing) Just <$> tryRecordType t++-- | Reduce a type and check whether it is a record type.+--   Succeeds only if type is not blocked by a meta var.+--   If yes, return its name, parameters, and definition.+--   If no, return the reduced type (unless it is blocked).+tryRecordType :: Type -> TCM (Either (Maybe Type) (QName, Args, Defn))+tryRecordType t = ifBlockedType t (\ _ _ -> return $ Left Nothing) $ \ t -> do+  let no = return $ Left $ Just t   case ignoreSharing $ unEl t of     Def r es -> do       let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es-      fmap (r,vs,) <$> isRecord r-    _        -> return Nothing+      caseMaybeM (isRecord r) no $ \ def -> return $ Right (r,vs,def)+    _ -> no  -- | The analogue of 'piApply'.  If @v@ is a value of record type @T@ --   with field @f@, then @projectType T f@ returns the type of @f v@.@@ -285,10 +295,10 @@   -- Construct @Δ@ as telescope.   -- Note @Γ₁, x:_ ⊢ Γ₂@, thus, @Γ₁, Γ' ⊢ [τ₀]Γ₂@ -      rev   = foldl (\ l (Dom ai (n, t)) -> Dom ai (show n, t) : l) []+      rev   = foldl (\ l (Dom ai (n, t)) -> Dom ai (nameToArgName n, t) : l) []       -- Use "f(x)" as variable name for the projection f(x).       s     = show x-      tel'  = mapAbsNames (\ f -> f ++ "(" ++ s ++ ")") tel+      tel'  = mapAbsNames (\ f -> stringToArgName $ argNameToString f ++ "(" ++ s ++ ")") tel       delta = telFromList $ rev gamma1 ++ telToList tel' ++ rev (applySubst tau0 gamma2)    return (delta, sigma, tau)@@ -442,22 +452,27 @@ --   contains garbage. isSingletonRecord' :: Bool -> QName -> Args -> TCM (Either MetaId (Maybe Term)) isSingletonRecord' regardIrrelevance r ps = do+  reportSLn "tc.meta.eta" 30 $ "Is " ++ show r ++ " a singleton record type?"   def <- getRecordDef r   emap (Con $ recConHead def) <$> check (recTel def `apply` ps)   where   check :: Telescope -> TCM (Either MetaId (Maybe [I.Arg Term]))-  check EmptyTel            = return $ Right $ Just []-  check (ExtendTel dom tel)-        | isIrrelevant dom && regardIrrelevance =-    underAbstraction dom tel $ \ tel ->-      emap (Arg (domInfo dom) garbage :) <$> check tel-  check (ExtendTel dom tel) = do-    isSing <- isSingletonType' regardIrrelevance $ unDom dom-    case isSing of-      Left mid       -> return $ Left mid-      Right Nothing  -> return $ Right Nothing-      Right (Just v) -> underAbstraction dom tel $ \ tel ->-        emap (Arg (domInfo dom) v :) <$> check tel+  check tel = do+    reportSDoc "tc.meta.eta" 30 $+      text "isSingletonRecord' checking telescope " <+> prettyTCM tel+    case tel of+      EmptyTel -> return $ Right $ Just []+      ExtendTel dom tel+        | isIrrelevant dom && regardIrrelevance -> do+          underAbstraction dom tel $ \ tel ->+            emap (Arg (domInfo dom) garbage :) <$> check tel+        | otherwise -> do+          isSing <- isSingletonType' regardIrrelevance $ unDom dom+          case isSing of+            Left mid       -> return $ Left mid+            Right Nothing  -> return $ Right Nothing+            Right (Just v) -> underAbstraction dom tel $ \ tel ->+              emap (Arg (domInfo dom) v :) <$> check tel   garbage :: Term   garbage = Sort Prop @@ -478,20 +493,9 @@     ifBlockedType t (\ m _ -> return $ Left m) $ \ t -> do       res <- isRecordType t       case res of-        Nothing         -> return $ Right Nothing-        Just (r, ps, _) -> do-          emap (abstract tel) <$> isSingletonRecord' regardIrrelevance r ps-{--    t <- reduceB $ unEl t-    case ignoreSharing <$> t of-      Blocked m _            -> return (Left m)-      NotBlocked (MetaV m _) -> return (Left m)-      NotBlocked (Def r es)  -> do-        let ps = fromMaybe __IMPOSSIBLE $ allApplyElims es-        ifM (isNothing <$> isRecord r) (return $ Right Nothing) $ do+        Just (r, ps, def) | recEtaEquality def -> do           emap (abstract tel) <$> isSingletonRecord' regardIrrelevance r ps-      _ -> return (Right Nothing)--}+        _ -> return $ Right Nothing  -- | Auxiliary function. emap :: (a -> b) -> Either c (Maybe a) -> Either c (Maybe b)
src/full/Agda/TypeChecking/Reduce.hs view
@@ -1,5 +1,8 @@-{-# LANGUAGE CPP, PatternGuards, TupleSections,-             TypeSynonymInstances, FlexibleInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.Reduce where
src/full/Agda/TypeChecking/Reduce/Monad.hs view
@@ -1,4 +1,8 @@-{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, TupleSections, FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TupleSections #-}+ module Agda.TypeChecking.Reduce.Monad   ( constructorForm   , enterClosure@@ -14,8 +18,10 @@ import Control.Applicative import Control.Monad.Reader import Control.Monad.Identity+ import qualified Data.Map as Map import Data.Maybe+ import Debug.Trace import System.IO.Unsafe @@ -75,10 +81,10 @@   let (i, s') = nextFresh s   localR (mapRedSt $ const s') (f i) -withFreshName :: Range -> String -> (Name -> ReduceM a) -> ReduceM a+withFreshName :: Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a withFreshName r s k = withFreshR $ \i -> k (mkName r i s) -withFreshName_ :: String -> (Name -> ReduceM a) -> ReduceM a+withFreshName_ :: ArgName -> (Name -> ReduceM a) -> ReduceM a withFreshName_ = withFreshName noRange  mkContextEntry :: Dom (Name, Type) -> (ContextEntry -> ReduceM a) -> ReduceM a
src/full/Agda/TypeChecking/Rules/Builtin.hs view
@@ -1,4 +1,7 @@-{-# LANGUAGE CPP, TupleSections, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+ module Agda.TypeChecking.Rules.Builtin (bindBuiltin, bindPostulatedName) where  import Control.Applicative
src/full/Agda/TypeChecking/Rules/Data.hs view
@@ -163,7 +163,7 @@       -- or a fresh sort meta set equal to a.       splitType :: Type -> TCM (Int, Sort)       splitType t = case ignoreSharing $ unEl t of-        Pi a b -> mapFst (+ 1) <$> do addCtxString (absName b) a $ splitType (absBody b)+        Pi a b -> mapFst (+ 1) <$> do addContext (absName b, a) $ splitType (absBody b)         Sort s -> return (0, s)         _      -> do           s <- newSortMeta@@ -269,8 +269,8 @@   -- Andreas, 2011-04-07 ignore relevance information in binding?!     | argInfoHiding info /= argInfoHiding info' = 	__IMPOSSIBLE__-    | otherwise = addCtx x arg $ bindParameters ps (absBody b) $ \tel s ->-		    ret (ExtendTel arg $ Abs (show x) tel) s+    | otherwise = addContext (x, arg) $ bindParameters ps (absBody b) $ \tel s ->+		    ret (ExtendTel arg $ Abs (nameToArgName x) tel) s bindParameters bs (El s (Shared p)) ret = bindParameters bs (El s $ derefPtr p) ret bindParameters (b : bs) t _ = __IMPOSSIBLE__ {- Andreas, 2012-01-17 Concrete.Definitions ensures number and hiding of parameters to be correct@@ -297,7 +297,7 @@   case ignoreSharing $ unEl t of     Pi dom b -> do       getSort (unDom dom) `leqSort` s-      addCtxString (absName b) dom $ fitsIn (absBody b) (raise 1 s)+      addContext (absName b, dom) $ fitsIn (absBody b) (raise 1 s)     _ -> return () -- getSort t `leqSort` s  -- Andreas, 2013-04-13 not necessary since constructor type ends in data type  -- | Return the parameters that share variables with the indices@@ -401,7 +401,7 @@  isCoinductive :: Type -> TCM (Maybe Bool) isCoinductive t = do-  El s t <- normalise t+  El s t <- reduce t   case ignoreSharing t of     Def q _ -> do       def <- getConstInfo q
src/full/Agda/TypeChecking/Rules/Decl.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, TupleSections #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}  module Agda.TypeChecking.Rules.Decl where @@ -448,21 +449,19 @@         A.CompiledJSPragma x ep ->           addJSCode x ep         A.StaticPragma x -> do-            def <- getConstInfo x-            case theDef def of-                Function{} -> do-                    markStatic x-                _ -> typeError $ GenericError "STATIC directive only works on functions"+          def <- getConstInfo x+          case theDef def of+            Function{} -> markStatic x+            _          -> typeError $ GenericError "STATIC directive only works on functions" 	A.OptionsPragma{} -> typeError $ GenericError $ "OPTIONS pragma only allowed at beginning of file, before top module declaration"-        A.EtaPragma r -> modifySignature eta+        A.EtaPragma r -> do+          unlessM (isJust <$> isRecord r) $+            typeError $ GenericError $ "ETA pragma is only applicable to records"+          modifySignature $ updateDefinition r $ updateTheDef $ setEta           where-            eta sig = sig { sigDefinitions = HMap.adjust setEta r defs }-              where-                setEta def = def { theDef = setEtad $ theDef def }-                setEtad d   = case d of-                  Record{}   -> d { recEtaEquality = True }-                  _          -> d-                defs	  = sigDefinitions sig+            setEta d = case d of+              Record{} -> d { recEtaEquality = True }+              _        -> __IMPOSSIBLE__  -- | Type check a bunch of mutual inductive recursive definitions. --
src/full/Agda/TypeChecking/Rules/Def.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}  module Agda.TypeChecking.Rules.Def where
src/full/Agda/TypeChecking/Rules/LHS.hs view
@@ -7,6 +7,7 @@ import Control.Applicative import Control.Monad import Control.Monad.State+ import Data.Traversable  import Agda.Interaction.Options@@ -259,7 +260,7 @@ bindLHSVars []        EmptyTel         ret = ret bindLHSVars (p : ps) (ExtendTel a tel) ret =   case namedArg p of-    A.VarP x      -> addCtx x a $ bindLHSVars ps (absBody tel) ret+    A.VarP x      -> addContext (x, a) $ bindLHSVars ps (absBody tel) ret     A.WildP _     -> bindDummy (absName tel)     A.ImplicitP _ -> bindDummy (absName tel)     A.AbsurdP pi  -> do@@ -283,11 +284,9 @@     A.LitP{}        -> __IMPOSSIBLE__     A.PatternSynP{} -> __IMPOSSIBLE__     where-      name "_" = freshNoName_-      name s   = freshName_ ("." ++ s)       bindDummy s = do-        x <- name s-        addCtx x a $ bindLHSVars ps (absBody tel) ret+        x <- if isUnderscore s then freshNoName_ else freshName_ ("." ++ argNameToString s)+        addContext (x, a) $ bindLHSVars ps (absBody tel) ret  -- | Bind as patterns bindAsPatterns :: [AsBinding] -> TCM a -> TCM a@@ -320,7 +319,7 @@                               -- Used only to construct a @with@ function; see 'stripwithClausePatterns'.       -> Telescope            -- Δ : The types of the pattern variables.       -> S.Substitution       -- σ : The patterns in form of a substitution Δ ⊢ σ : Γ-      -> [String]             -- Names for the variables in Δ, for binding the body.+      -> [ArgName]            -- Names for the variables in Δ, for binding the body.       -> [I.NamedArg Pattern] -- The patterns in internal syntax.       -> I.Arg Type           -- The type of the body. Is @bσ@ if @Γ@ is defined.                               -- 'Irrelevant' to indicate the rhs must be checked@@ -366,7 +365,7 @@      let rho = renamingR perm -- I'm not certain about this...         Perm n _ = perm-        xs  = [ "h" ++ show n | n <- [0..n - 1] ]+        xs  = [ stringToArgName $ "h" ++ show n | n <- [0..n - 1] ]     applyRelevanceToContext (getRelevance b') $ do       ret mgamma delta rho xs qs b' perm   where
src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}  module Agda.TypeChecking.Rules.LHS.Implicit where
src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs view
@@ -110,9 +110,9 @@     text "tel3 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel3)    -- Raise error if telescope cannot be ordered.-  let failToReorder = inTopContext $ addCtxStrings_ names3 $ do+  let failToReorder = inTopContext $ addContext names3 $ do         err <- sep [ text "Recursive telescope in left hand side:"-                   , fsep [ parens (text x <+> text ":" <+> prettyTCM t)+                   , fsep [ parens (text (argNameToString x) <+> text ":" <+> prettyTCM t)                           | (x, t) <- zip names3 tel3 ]                    ]         typeError $ GenericError $ show err
src/full/Agda/TypeChecking/Rules/LHS/Problem.hs view
@@ -1,4 +1,9 @@-{-# LANGUAGE CPP, FlexibleInstances, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+-- {-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+ module Agda.TypeChecking.Rules.LHS.Problem where  import Control.Monad.Error
src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, TupleSections #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}  module Agda.TypeChecking.Rules.LHS.ProblemRest where @@ -27,7 +28,7 @@ useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList   where     dummy = A.WildP __IMPOSSIBLE__-    ren (A.VarP x) (Dom info (_, a)) | notHidden info = Dom info (show x, a)+    ren (A.VarP x) (Dom info (_, a)) | notHidden info = Dom info (nameToArgName x, a)     -- Andreas, 2013-03-13: inserted the following line in the hope to fix issue 819     -- but it does not do the job, instead, it puts a lot of "_"s     -- instead of more sensible names into error messages.@@ -40,12 +41,6 @@ noProblemRest :: Problem -> Bool noProblemRest (Problem _ _ _ (ProblemRest ps _)) = null ps -{- UNUSED and OUTDATED--- | Get the type of clause.  Only valid if 'noProblemRest'.-typeFromProblem :: Problem -> Type-typeFromProblem (Problem _ _ _ (ProblemRest _ a)) = a--}- -- | Construct an initial 'split' 'Problem' from user patterns. --   Example: --   @@@ -108,11 +103,6 @@            ]          ]   return problem--{--todoProblemRest :: ProblemRest-todoProblemRest = mempty--}  -- | Try to move patterns from the problem rest into the problem. --   Possible if type of problem rest has been updated to a function type.
src/full/Agda/TypeChecking/Rules/LHS/Split.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards, ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}  module Agda.TypeChecking.Rules.LHS.Split where @@ -146,7 +148,7 @@     -- Stripping initial lambdas from a normalized term     stripLambdas :: Term -> TCM Term     stripLambdas v = case ignoreSharing v of-        Lam _ b -> addCtxString_ (absName b) $ stripLambdas (absBody b)+        Lam _ b -> addContext (absName b) $ stripLambdas (absBody b)         v       -> return v      -- | In @splitP aps iqs tel@,@@ -174,9 +176,11 @@       case asView $ namedArg p of          -- Case: projection pattern.  That's an error.-        (_, p') | Just{} <- isProjP p' -> do-           typeError $ CannotEliminateWithPattern p (telePi tel0 $ unArg $ restType pr)-+        --(_, p') | Just{} <- isProjP p' -> do+        (_, A.DefP _ d ps) -> typeError $+          if null ps+          then CannotEliminateWithPattern p (telePi tel0 $ unArg $ restType pr)+          else IllformedProjectionPattern $ namedArg p         -- Case: literal pattern 	(xs, p@(A.LitP lit))  -> do           -- Note that, in the presence of --without-K, this branch is
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs view
@@ -1,6 +1,14 @@-{-# LANGUAGE CPP, MultiParamTypeClasses, FlexibleInstances, TupleSections,-    PatternGuards, GeneralizedNewtypeDeriving, DeriveDataTypeable,-    DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.Rules.LHS.Unify where @@ -1054,7 +1062,7 @@   (t, sh) <- shapeViewHH =<< liftTCM (traverse reduce t)   case sh of     PiSh a b  -> absV a (absName b) <$> telViewUpToHH (n-1) (absBody b)-    FunSh a b -> absV a "_" <$> telViewUpToHH (n-1) (raise 1 b)+    FunSh a b -> absV a underscore <$> telViewUpToHH (n-1) (raise 1 b)     _         -> return $ TelV EmptyTel t   where     absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t
src/full/Agda/TypeChecking/Rules/Record.hs view
@@ -110,14 +110,14 @@         Just c  -> return (True, c, i)         Nothing -> do           m <- killRange <$> currentModule-          c <- qualify m <$> freshName_ "recCon-NOT-PRINTED"+          c <- qualify m <$> freshName_ ("recCon-NOT-PRINTED" :: String)           return (False, c, i)        -- Add record type to signature.       reportSDoc "tc.rec" 15 $ text "adding record type to signature"        let getName :: A.Declaration -> [A.Arg QName]-          getName (A.Field _ x arg)    = [fmap (const x) arg]+          getName (A.Field _ x arg)    = [x <$ arg] 	  getName (A.ScopedDecl _ [f]) = getName f 	  getName _		       = [] @@ -161,8 +161,8 @@                          }        -- Check that the fields fit inside the sort-      let dummy = var 0  -- We're only interested in the sort here-      telePi ftel (El s dummy) `fitsIn` s+      let dummy = Sort Prop  -- We're only interested in the sort here+      telePi ftel (El (raise (size ftel) s) dummy) `fitsIn` s        {- Andreas, 2011-04-27 WRONG because field types are checked again          and then non-stricts should not yet be irrelevant@@ -314,7 +314,7 @@           rel      = getRelevance ai           -- the recursive call           recurse  = checkProjs (abstract ftel1 $ ExtendTel (Dom ai t)-                                 $ Abs (show $ qnameName projname) EmptyTel)+                                 $ Abs (nameToArgName $ qnameName projname) EmptyTel)                                 (ftel2 `absApp` projcall) fs        reportSDoc "tc.rec.proj" 25 $ nest 2 $ text "finalt=" <+> do
src/full/Agda/TypeChecking/Rules/Term.hs view
@@ -1,5 +1,10 @@-{-# LANGUAGE CPP, PatternGuards, TupleSections, NamedFieldPuns,-      MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  module Agda.TypeChecking.Rules.Term where @@ -86,7 +91,7 @@     A.Fun i (Arg info t) b -> do       a <- Dom info <$> isType_ t       b <- isType_ b-      return $ El (sLub (getSort $ unDom a) (getSort b)) (Pi (convColor a) (NoAbs "_" b))+      return $ El (sLub (getSort $ unDom a) (getSort b)) (Pi (convColor a) (NoAbs underscore b))     A.Pi _ tel e -> do       checkTelescope_ tel $ \tel -> do         t   <- instantiateFull =<< isType_ e@@ -252,12 +257,11 @@         -- check.         (pid, argT) <- newProblem $ isTypeEqualTo typ (unDom arg)         v <- add y (Dom (setRelevance r' info) argT) $ checkExpr body btyp-        blockTermOnProblem target (Lam info $ Abs (show xc) v) pid+        blockTermOnProblem target (Lam info $ Abs (nameToArgName x) v) pid       where         [x] = xs-        xc  = nameConcrete x-        add y | isNoName xc = addCtxString y-              | otherwise   = addCtx x+        add y dom | isNoName x = addContext (y, dom)+                  | otherwise  = addContext (x, dom)     useTargetType _ _ = __IMPOSSIBLE__  -- | @checkAbsurdLambda i h e t@ checks absurd lambda against type @t@.@@ -277,7 +281,7 @@ --          return $ Lam info' absurdBody           -- Add helper function           top <- currentModule-          aux <- qualify top <$> freshName (getRange i) absurdLambdaName+          aux <- qualify top <$> freshName_ (getRange i, absurdLambdaName)           -- if we are in irrelevant position, the helper function           -- is added as irrelevant           rel <- asks envRelevance@@ -622,11 +626,6 @@                 q <- quoteTerm =<< normalise et                 ty <- el primAgdaTerm                 coerce q ty t--	  | A.Unquote _ <- unScope q ->-	     do e1 <- checkExpr (namedThing e) =<< el primAgdaTerm-	        e2 <- unquote e1-                checkTerm e2 t         A.Quote _ -> typeError $ GenericError "quote must be applied to a defined name"         A.QuoteTerm _ -> typeError $ GenericError "quoteTerm must be applied to a term"         A.Unquote _ -> typeError $ GenericError "unquote must be applied to a term"@@ -657,7 +656,7 @@ 	    a' <- isType_ a 	    b' <- isType_ b 	    s <- reduce $ getSort a' `sLub` getSort b'-	    coerce (Pi (convColor $ Dom info a') (NoAbs "_" b')) (sort s) t+	    coerce (Pi (convColor $ Dom info a') (NoAbs underscore b')) (sort s) t 	A.Set _ n    -> do           n <- ifM typeInType (return 0) (return n) 	  coerce (Sort $ mkType n) (sort $ mkType $ n + 1) t@@ -781,6 +780,16 @@               e' = A.lambdaLiftExpr (map unArg ns) (A.substExpr s p')           checkExpr e' t +    -- Subcase: unquote+    A.Unquote _+      | [arg] <- args -> do+          v <- unquote =<< checkExpr (namedArg arg) =<< el primAgdaTerm+          checkTerm v t+      | arg : args <- args -> do+          v  <- unquote =<< checkExpr (namedArg arg) =<< el primAgdaTerm+          e' <- withShowAllArguments $ reify (v :: Term)    -- TODO: use checkInternal (but see comment on checkTerm)+          checkHeadApplication e t e' $ map convColor args+     -- Subcase: defined symbol or variable.     _ -> checkHeadApplication e t hd $ map convColor args @@ -1401,7 +1410,7 @@     p <- expandPatternSynonyms p     (v, t) <- inferExpr e     let -- construct a type  t -> dummy  for use in checkLeftHandSide-        t0 = El (getSort t) $ Pi (Dom defaultArgInfo t) (NoAbs "_" typeDontCare)+        t0 = El (getSort t) $ Pi (Dom defaultArgInfo t) (NoAbs underscore typeDontCare)         p0 = Arg defaultArgInfo (Named Nothing p)     reportSDoc "tc.term.let.pattern" 10 $ vcat       [ text "let-binding pattern p at type t"
src/full/Agda/TypeChecking/Serialise.hs view
@@ -31,7 +31,7 @@ import Control.Monad.Error import Data.Array.IArray import Data.Word-import Data.ByteString.Lazy as L+import qualified Data.ByteString.Lazy as L import Data.Hashable import qualified Data.HashTable.IO as H import Data.Int (Int32)@@ -166,7 +166,7 @@ -- | Encodes something. To ensure relocatability file paths in -- positions are replaced with module names. -encode :: EmbPrj a => a -> TCM ByteString+encode :: EmbPrj a => a -> TCM L.ByteString encode a = do     fileMod <- sourceToModule     newD@(Dict nD sD iD dD _ _ _ _ _ stats _) <- liftIO $ emptyDict fileMod@@ -186,7 +186,7 @@     l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h     benchSort = billTo [Bench.Serialization, Bench.Sort] . liftIO --- encode :: EmbPrj a => a -> TCM ByteString+-- encode :: EmbPrj a => a -> TCM L.ByteString -- encode a = do --     fileMod <- sourceToModule --     (x, shared, total) <- liftIO $ do@@ -207,7 +207,7 @@ --   Reimplementing it in terms of the new function. The new Decoder type contains --   strict byte strings so we need to be careful not to feed the entire lazy byte --   string to the decoder at once.-runGetState :: B.Get a -> ByteString -> B.ByteOffset -> (a, ByteString, B.ByteOffset)+runGetState :: B.Get a -> L.ByteString -> B.ByteOffset -> (a, L.ByteString, B.ByteOffset) runGetState g s n = feed (B.runGetIncremental g) (L.toChunks s)   where     feed (B.Done s n' x) ss     = (x, L.fromChunks (s : ss), n + n')@@ -220,7 +220,7 @@ -- Returns 'Nothing' if the input does not start with the right magic -- number or some other decoding error is encountered. -decode :: EmbPrj a => ByteString -> TCM (Maybe a)+decode :: EmbPrj a => L.ByteString -> TCM (Maybe a) decode s = do   mf   <- stModuleToSource <$> get   incs <- getIncludeDirs@@ -270,10 +270,10 @@    noResult s = return (Nothing, Left $ GenericError s) -encodeInterface :: Interface -> TCM ByteString+encodeInterface :: Interface -> TCM L.ByteString encodeInterface i = L.append hashes <$> encode i   where-    hashes :: ByteString+    hashes :: L.ByteString     hashes = B.runPut $ B.put (iSourceHash i) >> B.put (iFullHash i)  -- | Encodes something. To ensure relocatability file paths in@@ -287,10 +287,10 @@ -- Returns 'Nothing' if the file does not start with the right magic -- number or some other decoding error is encountered. -decodeInterface :: ByteString -> TCM (Maybe Interface)+decodeInterface :: L.ByteString -> TCM (Maybe Interface) decodeInterface s = decode $ L.drop 16 s -decodeHashes :: ByteString -> Maybe (Hash, Hash)+decodeHashes :: L.ByteString -> Maybe (Hash, Hash) decodeHashes s   | L.length s < 16 = Nothing   | otherwise       = Just $ B.runGet getH $ L.take 16 s
src/full/Agda/TypeChecking/SizedTypes.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+ module Agda.TypeChecking.SizedTypes where  import Control.Monad.Error
src/full/Agda/TypeChecking/SizedTypes/Solve.hs view
@@ -1,8 +1,15 @@-{-# LANGUAGE CPP, PatternGuards, TupleSections, ScopedTypeVariables,-  FlexibleInstances, TypeSynonymInstances,-  MultiParamTypeClasses,-  GeneralizedNewtypeDeriving, DeriveFunctor, DeriveFoldable, DeriveTraversable,-  StandaloneDeriving #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}  -- | Solving size constraints under hypotheses. --
src/full/Agda/TypeChecking/SizedTypes/Tests.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE TemplateHaskell, NoMonomorphismRestriction, ScopedTypeVariables #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}  module Agda.TypeChecking.SizedTypes.Tests where
src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs view
@@ -1,7 +1,14 @@-{-# LANGUAGE CPP, TupleSections, PatternGuards, NoMonomorphismRestriction, ScopedTypeVariables,-  TypeSynonymInstances, FlexibleInstances, DeriveFunctor,-  MultiParamTypeClasses #-}--- {-# LANGUAGE UndecidableInstances, OverlappingInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+-- {-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+-- {-# LANGUAGE UndecidableInstances #-}  module Agda.TypeChecking.SizedTypes.WarshallSolver where
src/full/Agda/TypeChecking/Substitute.hs view
@@ -1,15 +1,23 @@-{-# LANGUAGE CPP, PatternGuards, TupleSections,-    TypeSynonymInstances, FlexibleInstances, OverlappingInstances,-    DeriveDataTypeable, DeriveFunctor, StandaloneDeriving #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+ module Agda.TypeChecking.Substitute where  import Control.Arrow ((***)) -import Data.Typeable (Typeable)+import Data.Function+import Data.Functor import Data.List hiding (sort, drop) import qualified Data.List as List-import Data.Function import Data.Map (Map)+import Data.Typeable (Typeable)  import Debug.Trace (trace) @@ -444,8 +452,8 @@     where         tel   = foldr (\(Common.Arg info x) -> ExtendTel (Common.Dom info $ sort Prop) . Abs x)                       EmptyTel-              $ zipWith (fmap . const) names args-        names = cycle $ map (:[]) ['a'..'z']+              $ zipWith (<$) names args+        names = cycle $ map (stringToArgName . (:[])) ['a'..'z']  --------------------------------------------------------------------------- -- * Explicit substitutions@@ -718,9 +726,9 @@   deriving (Typeable, Show, Eq, Ord, Functor)  type ListTel' a = [Dom (a, Type)]-type ListTel = ListTel' String+type ListTel = ListTel' ArgName -telFromList' :: (a -> String) -> ListTel' a -> Telescope+telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope telFromList' f = foldr extTel EmptyTel   where     extTel (Common.Dom info (x, a)) = ExtendTel (Common.Dom info a) . Abs (f x)@@ -740,7 +748,7 @@ bindsToTel' f (x:xs) t = fmap (f x,) t : bindsToTel' f xs (raise 1 t)  bindsToTel :: [Name] -> Dom Type -> ListTel-bindsToTel = bindsToTel' (show . nameConcrete)+bindsToTel = bindsToTel' nameToArgName  telView' :: Type -> TelView telView' t = case ignoreSharing $ unEl t of@@ -750,7 +758,7 @@     absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t  -- | @mkPi dom t = telePi (telFromList [dom]) t@-mkPi :: Dom (String, Type) -> Type -> Type+mkPi :: Dom (ArgName, Type) -> Type -> Type mkPi (Common.Dom info (x, a)) b = el $ Pi (Common.Dom info a) (mkAbs x b)   where     el = El $ dLub (getSort a) (Abs x (getSort b)) -- dLub checks x freeIn@@ -827,7 +835,7 @@ absBody (Abs   _ v) = v absBody (NoAbs _ v) = raise 1 v -mkAbs :: (Subst a, Free a) => String -> a -> Abs a+mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a mkAbs x v | 0 `freeIn` v = Abs x v           | otherwise    = NoAbs x (raise (-1) v)
src/full/Agda/TypeChecking/SyntacticEquality.hs view
@@ -1,5 +1,10 @@-{-# LANGUAGE CPP, PatternGuards, TupleSections,-             TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+ -- | A syntactic equality check that takes meta instantiations into account, --   but does not reduce.  It replaces --   @
src/full/Agda/TypeChecking/Telescope.hs view
@@ -3,6 +3,7 @@ module Agda.TypeChecking.Telescope where  import Control.Applicative+ import Data.List  import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)@@ -63,7 +64,7 @@  -- | Unflatten: turns a flattened telescope into a proper telescope. Must be --   properly ordered.-unflattenTel :: [String] -> [Dom Type] -> Telescope+unflattenTel :: [ArgName] -> [Dom Type] -> Telescope unflattenTel []	  []	        = EmptyTel unflattenTel (x : xs) (a : tel) = ExtendTel a' (Abs x tel')   where@@ -74,10 +75,10 @@ unflattenTel (_ : _) [] = __IMPOSSIBLE__  -- | Get the suggested names from a telescope-teleNames :: Telescope -> [String]+teleNames :: Telescope -> [ArgName] teleNames = map (fst . unDom) . telToList -teleArgNames :: Telescope -> [Arg String]+teleArgNames :: Telescope -> [Arg ArgName] teleArgNames = map (argFromDom . fmap fst) . telToList  teleArgs :: Telescope -> Args
src/full/Agda/TypeChecking/Test/Generators.hs view
@@ -1,14 +1,15 @@-{-# LANGUAGE CPP, MultiParamTypeClasses,-             FunctionalDependencies, UndecidableInstances,-             TypeSynonymInstances, FlexibleInstances-  #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}  module Agda.TypeChecking.Test.Generators where  import Control.Applicative import Control.Monad.State import qualified Data.List as List (sort, nub)-import Agda.Utils.QuickCheck hiding (Args)  import Agda.Syntax.Position import Agda.Syntax.Common as Common@@ -16,8 +17,11 @@ import Agda.Syntax.Fixity import Agda.Syntax.Internal as I import qualified Agda.Syntax.Concrete.Name as C+ import Agda.TypeChecking.Free import Agda.TypeChecking.Substitute++import Agda.Utils.QuickCheck hiding (Args) import Agda.Utils.TestHelpers import qualified Agda.Utils.VarSet as Set @@ -127,7 +131,7 @@ extendWithTelConf :: Telescope -> TermConfiguration -> TermConfiguration extendWithTelConf tel conf = foldr (const extendConf) conf (telToList tel) -makeConfiguration :: [String] -> [String] -> [String] -> [Nat] -> TermConfiguration+makeConfiguration :: [RawName] -> [RawName] -> [RawName] -> [Nat] -> TermConfiguration makeConfiguration ds cs ps vs = TermConf   { tcDefinedNames     = defs   , tcConstructorNames = cons@@ -199,7 +203,8 @@   genC conf = (\ (h, a) -> Dom (setHiding h defaultArgInfo) a) <$> genC conf  instance GenC a => GenC (Abs a) where-  genC conf = Abs "x" <$> genC (extendConf conf)+  genC conf = Abs x <$> genC (extendConf conf)+    where x = stringToArgName "x"  instance GenC a => GenC (Elim' a) where   genC conf = frequency [ (applyF, Apply <$> genC conf)@@ -326,9 +331,9 @@   vs <- listOf natural   return $ makeConfiguration ds cs ps vs   where-    defs = [ [c] | c <- ['a'..'n'] ++ ['r'..'z'] ]-    cons = [ [c] | c <- ['A'..'Z'] ]-    projs= [ [c] | c <- ['o'..'q'] ]+    defs = [ stringToRawName [c] | c <- ['a'..'n'] ++ ['r'..'z'] ]+    cons = [ stringToRawName [c] | c <- ['A'..'Z'] ]+    projs= [ stringToRawName [c] | c <- ['o'..'q'] ]  instance Arbitrary TermConfiguration where   arbitrary   = genConf
src/full/Agda/TypeChecking/With.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+ module Agda.TypeChecking.With where  import Control.Applicative
src/full/Agda/Utils/BiMap.hs view
@@ -1,7 +1,11 @@ -- | Finite bijections (implemented as a pair of maps). -{-# LANGUAGE TemplateHaskell, TupleSections, PatternGuards, FlexibleInstances,-  GeneralizedNewtypeDeriving, DeriveDataTypeable #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}  module Agda.Utils.BiMap where
src/full/Agda/Utils/Cluster.hs view
@@ -1,5 +1,7 @@-{-# LANGUAGE ScopedTypeVariables, TupleSections, TemplateHaskell,-  FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}  -- | Create clusters of non-overlapping things. @@ -45,10 +47,6 @@   let m = Map.unionsWith (++) cas   -- Return the values of the map   return $ Map.elems m---- | Forgotten 'Functor' instance in package 'equivalence'.-instance Monad m => Functor (EquivT s x y m) where-  fmap f x = x >>= return . f  ------------------------------------------------------------------------ -- * Properties
src/full/Agda/Utils/Favorites.hs view
@@ -1,5 +1,8 @@-{-# LANGUAGE CPP, TemplateHaskell, NoImplicitPrelude,-      GeneralizedNewtypeDeriving, DeriveFoldable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE TemplateHaskell #-}  -- | Maintaining a list of favorites of some partially ordered type. --   Only the best elements are kept.
src/full/Agda/Utils/FileName.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, DeriveDataTypeable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}  {-| Operations on file names. -} module Agda.Utils.FileName
src/full/Agda/Utils/List.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, TemplateHaskell, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TemplateHaskell #-}  {-| Utitlity functions on lists. -}
src/full/Agda/Utils/Maybe.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP #-}+-- {-# LANGUAGE CPP #-}  -- | Extend 'Data.Maybe' by common operations for the 'Maybe' type. --
src/full/Agda/Utils/Maybe/Strict.hs view
@@ -1,10 +1,12 @@-{-# LANGUAGE CPP,-  MultiParamTypeClasses,-  DeriveDataTypeable, StandaloneDeriving #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}  #if __GLASGOW_HASKELL__ >= 706 {-# LANGUAGE DeriveGeneric #-} #endif++{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneDeriving #-}  {-# OPTIONS_GHC -fno-warn-orphans #-}
src/full/Agda/Utils/Monad.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP, FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}  module Agda.Utils.Monad     ( module Agda.Utils.Monad
+ src/full/Agda/Utils/Null.hs view
@@ -0,0 +1,43 @@+-- | Overloaded @null@ and @empty@ for collections and sequences.++module Agda.Utils.Null where++import Data.ByteString.Char8 (ByteString)+import qualified Data.ByteString.Char8 as ByteString+import qualified Data.List as List+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Sequence (Seq)+import qualified Data.Sequence as Seq+import Data.Set (Set)+import qualified Data.Set as Set++class Null a where+  empty :: a+  null  :: a -> Bool+  -- ^ Satisfying @null empty == True@.++instance Null ByteString where+  empty = ByteString.empty+  null  = ByteString.null++instance Null [a] where+  empty = []+  null  = List.null++instance Null (Map k a) where+  empty = Map.empty+  null  = Map.null++instance Null (Seq a) where+  empty = Seq.empty+  null  = Seq.null++instance Null (Set a) where+  empty = Set.empty+  null  = Set.null++-- instance Null (Maybe a) where+--   empty = Nothing+--   null Nothing  = True+--   null (Just a) = False
src/full/Agda/Utils/PartialOrd.hs view
@@ -1,9 +1,12 @@-{-# LANGUAGE TemplateHaskell,-      FlexibleInstances, GeneralizedNewtypeDeriving, DeriveFunctor #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TemplateHaskell #-}  module Agda.Utils.PartialOrd where  import Data.Functor+import Data.Maybe import Data.Monoid import Data.List import Data.Set (Set)@@ -26,6 +29,31 @@   | POAny -- ^ No information (incomparable).   deriving (Eq, Show, Enum, Bounded) +-- | Comparing the information content of two elements of+--   'PartialOrdering'.  More precise information is smaller.+--+--   Includes equality: @x `leqPO` x == True@.++leqPO :: PartialOrdering -> PartialOrdering -> Bool++leqPO _   POAny = True++leqPO POLT POLT = True+leqPO POLT POLE = True++leqPO POLE POLE = True++leqPO POEQ POLE = True+leqPO POEQ POEQ = True+leqPO POEQ POGE = True++leqPO POGE POGE = True++leqPO POGT POGT = True+leqPO POGT POGE = True++leqPO _ _ = False+ -- | Opposites. -- --   @related a po b@ iff @related b (oppPO po) a@.@@ -38,57 +66,63 @@ oppPO POGT  = POLT oppPO POAny = POAny --- | What if either of two facts hold?---   @x R y || x S y@+-- | Combining two pieces of information (picking the least information).+--   Used for the dominance ordering on tuples.+--+--   @orPO@ is associative, commutative, and idempotent.+--   @orPO@ has dominant element @POAny@, but no neutral element.+ orPO :: PartialOrdering -> PartialOrdering -> PartialOrdering  orPO POAny _   = POAny   -- Shortcut if no information on first. -orPO POLT POLT = POLT+orPO POLT POLT = POLT   -- idempotent orPO POLT POLE = POLE orPO POLT POEQ = POLE  orPO POLE POLT = POLE-orPO POLE POLE = POLE+orPO POLE POLE = POLE   -- idempotent orPO POLE POEQ = POLE  orPO POEQ POLT = POLE orPO POEQ POLE = POLE-orPO POEQ POEQ = POEQ+orPO POEQ POEQ = POEQ   -- idempotent orPO POEQ POGE = POGE orPO POEQ POGT = POGE  orPO POGE POEQ = POGE-orPO POGE POGE = POGE+orPO POGE POGE = POGE   -- idempotent orPO POGE POGT = POGE  orPO POGT POEQ = POGE orPO POGT POGE = POGE-orPO POGT POGT = POGT+orPO POGT POGT = POGT   -- idempotent  orPO _    _    = POAny  -- | Chains (transitivity) @x R y S z@.---   Also: conjunction (trying to get the best information out).+--+--   @seqPO@ is associative, commutative, and idempotent.+--   @seqPO@ has dominant element @POAny@ and neutral element (unit) @POEQ@.  seqPO POAny _   = POAny  -- Shortcut if no information on first. seqPO POEQ p    = p      -- No need to look at second if first is neutral. -seqPO POLT POLT = POLT+seqPO POLT POLT = POLT   -- idempotent seqPO POLT POLE = POLT-seqPO POLT POEQ = POLT+seqPO POLT POEQ = POLT   -- unit  seqPO POLE POLT = POLT-seqPO POLE POLE = POLE-seqPO POLE POEQ = POLE+seqPO POLE POLE = POLE   -- idempotent+seqPO POLE POEQ = POLE   -- unit -seqPO POGE POEQ = POGE-seqPO POGE POGE = POGE+seqPO POGE POEQ = POGE   -- unit+seqPO POGE POGE = POGE   -- idempotent seqPO POGE POGT = POGT -seqPO POGT POEQ = POGT+seqPO POGT POEQ = POGT   -- unit seqPO POGT POGE = POGT-seqPO POGT POGT = POGT+seqPO POGT POGT = POGT   -- idempotent  seqPO _    _    = POAny @@ -139,8 +173,16 @@ --   @related a o b@ holds iff @comparable a b@ is contained in @o@.  related :: PartialOrd a => a -> PartialOrdering -> a -> Bool-related a o b = null $ toOrderings (comparable a b) \\ toOrderings o+related a o b = comparable a b `leqPO` o +-- * Totally ordered types.++instance PartialOrd Int where+  comparable = comparableOrd++instance PartialOrd Integer where+  comparable = comparableOrd+ -- * Generic partially ordered types.  instance PartialOrd () where@@ -172,7 +214,7 @@  instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where   comparable (x1, x2) (y1, y2) =-    comparable x1 y1 `mappend`+    comparable x1 y1 `orPO`     comparable x2 y2  -- | Pointwise comparison wrapper.@@ -180,15 +222,23 @@ newtype Pointwise a = Pointwise { pointwise :: a }   deriving (Eq, Show, Functor) --- | Lifting the pointwise ordering for tuples to lists.+-- | The pointwise ordering for lists of the same length. -----   There are other partial orderings for lists, e.g., prefix, sublist, subset.+--   There are other partial orderings for lists,+--   e.g., prefix, sublist, subset, lexicographic, simultaneous order.  instance PartialOrd a => PartialOrd (Pointwise [a]) where-  comparable xs ys = comparable (unconsPointwise $ pointwise xs)-                                (unconsPointwise $ pointwise ys)-    where unconsPointwise []       = Nothing-          unconsPointwise (x : xs) = Just (x, Pointwise xs)+  comparable (Pointwise xs) (Pointwise ys) = loop Nothing xs ys+    -- We need an accumulator since @orPO@ does not have a neutral element.+    where+      loop mo []     []     = fromMaybe POEQ mo+      loop _  []     ys     = POAny+      loop _  xs     []     = POAny+      loop mo (x:xs) (y:ys) =+        let o = comparable x y in+        case maybe o (orPO o) mo of+          POAny -> POAny+          o     -> loop (Just o) xs ys  -- | Inclusion comparison wrapper. @@ -258,7 +308,7 @@   deriving (Eq, Ord, PartialOrd, Show)  instance Arbitrary ISet where-  arbitrary = ISet . Inclusion . Set.fromList <$> arbitrary+  arbitrary = ISet . Inclusion . Set.fromList <$> listOf (choose (0, 8))  -- | Any two elements are 'related' in the way 'comparable' computes. prop_comparable_related (ISet a) (ISet b) =@@ -271,6 +321,10 @@ -- | Auxiliary function: lists to sets = sorted duplicate-free lists. sortUniq = Set.toAscList . Set.fromList +-- | 'leqPO' is inclusion of the associated 'Ordering' sets.+prop_leqPO_sound p q =+  (p `leqPO` q) == null (toOrderings p \\ toOrderings q)+ -- | 'orPO' amounts to the union of the associated 'Ordering' sets. --   Except that 'orPO POLT POGT == POAny' which should also include 'POEQ'. prop_orPO_sound p q =@@ -279,9 +333,12 @@ -- | 'orPO' is associative. prop_associative_orPO = associative orPO --- | 'orPO' is communtative.+-- | 'orPO' is commutative. prop_commutative_orPO = commutative orPO +-- | 'orPO' is idempotent.+prop_idempotent_orPO = idempotent orPO+ -- | The dominant element wrt. 'orPO' is 'POAny'. prop_zero_orPO = isZero POAny orPO @@ -306,6 +363,9 @@  -- | 'seqPO' is also commutative. prop_commutative_seqPO = commutative seqPO++-- | 'seqPO' is idempotent.+prop_idempotent_seqPO = idempotent seqPO  -- | 'seqPO' distributes over 'orPO'. prop_distributive_seqPO_orPO = distributive seqPO orPO
src/full/Agda/Utils/Permutation.hs view
@@ -1,4 +1,9 @@-{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+ module Agda.Utils.Permutation where  import Prelude hiding (drop)
src/full/Agda/Utils/QuickCheck.hs view
@@ -15,7 +15,3 @@  quickCheckWith' :: Testable prop => Args -> prop -> IO Bool quickCheckWith' args p = fmap isSuccess $ quickCheckWithResult args p--divPropSize :: Int -> Property -> Property-divPropSize k (MkProperty prop) =-  MkProperty $ sized $ \n -> resize (n `div` k) prop
src/full/Agda/Utils/Suffix.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, PatternGuards #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+ module Agda.Utils.Suffix where  import Data.Char
src/full/Agda/Utils/TestHelpers.hs view
@@ -5,6 +5,7 @@   ( -- * Algebraic properties     associative   , commutative+  , idempotent   , isZero   , identity   , leftDistributive@@ -46,6 +47,14 @@             -> a -> a -> Bool commutative (+) = \x y ->   x + y == y + x++-- | Is the operator idempotent?++idempotent :: (Arbitrary a, Eq a, Show a)+            => (a -> a -> a)+            -> a -> Bool+idempotent (/\) = \ x ->+  (x /\ x) == x  -- | Is the element a zero for the operator?
src/full/Agda/Utils/Trie.hs view
@@ -1,7 +1,10 @@ -- | Strict tries (based on 'Data.Map.Strict' and 'Agda.Utils.Maybe.Strict'). -{-# LANGUAGE CPP, TupleSections, PatternGuards, BangPatterns,-  GeneralizedNewtypeDeriving #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TupleSections #-}  module Agda.Utils.Trie   ( Trie