Agda 2.4.2.1 → 2.4.2.2

raw patch · 29 files changed

+905/−499 lines, 29 filesdep ~Agdadep ~hashtablesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: Agda, hashtables

API changes (from Hackage documentation)

Files

• Agda.cabal +6/−5
• CHANGELOG +22/−4
• src/data/emacs-mode/agda2-mode.el +1/−1
• src/full/Agda/Compiler/Epic/Injection.hs +11/−7
• src/full/Agda/Compiler/JS/Compiler.hs +1/−1
• src/full/Agda/Interaction/BasicOps.hs +14/−2
• src/full/Agda/Syntax/Internal.hs +13/−7
• src/full/Agda/Syntax/Internal/Pattern.hs +66/−40
• src/full/Agda/Tests.hs +2/−0
• src/full/Agda/TypeChecking/Abstract.hs +1/−1
• src/full/Agda/TypeChecking/CheckInternal.hs +14/−1
• src/full/Agda/TypeChecking/Coverage.hs +4/−3
• src/full/Agda/TypeChecking/Injectivity.hs +1/−1
• src/full/Agda/TypeChecking/Polarity.hs +1/−1
• src/full/Agda/TypeChecking/Quote.hs +0/−360
• src/full/Agda/TypeChecking/Reduce.hs +11/−0
• src/full/Agda/TypeChecking/Reduce/Monad.hs +1/−2
• src/full/Agda/TypeChecking/Rules/Decl.hs +1/−0
• src/full/Agda/TypeChecking/Rules/Def.hs +4/−0
• src/full/Agda/TypeChecking/Rules/LHS.hs +93/−20
• src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +37/−26
• src/full/Agda/TypeChecking/Rules/Record.hs +5/−0
• src/full/Agda/TypeChecking/Rules/Term.hs +1/−0
• src/full/Agda/TypeChecking/Telescope.hs +19/−11
• src/full/Agda/TypeChecking/Unquote.hs +403/−0
• src/full/Agda/Utils/FileName.hs +1/−1
• src/full/Agda/Utils/Permutation.hs +40/−1
• src/full/Agda/Utils/Permutation/Tests.hs +117/−0
• src/full/Agda/Utils/VarSet.hs +15/−4

@@ -1,5 +1,5 @@ name:            Agda-version:         2.4.2.1+version:         2.4.2.2 cabal-version:   >= 1.8 build-type:      Custom license:         OtherLicense@@ -33,7 +33,6 @@   policy, because it is not intended to be used by third-party   packages. tested-with:        GHC == 7.0.4-                    GHC == 7.2.2                     GHC == 7.4.2                     GHC == 7.6.3                     GHC == 7.8.3@@ -57,7 +56,7 @@ source-repository this   type:     git   location: https://github.com/agda/agda-  tag:      2.4.2.1+  tag:      2.4.2.2  flag cpphs   default:     True@@ -331,6 +330,7 @@                     Agda.TypeChecking.Test.Generators                     Agda.TypeChecking.Tests --                    Agda.TypeChecking.UniversePolymorphism -- RETIRED+                    Agda.TypeChecking.Unquote                     Agda.TypeChecking.With                     Agda.Utils.AssocList                     Agda.Utils.Bag@@ -363,6 +363,7 @@                     Agda.Utils.Null                     Agda.Utils.PartialOrd                     Agda.Utils.Permutation+                    Agda.Utils.Permutation.Tests                     Agda.Utils.Pointer                     Agda.Utils.Pointed                     Agda.Utils.Pretty@@ -419,7 +420,7 @@   -- 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+  --    ghc-options:    -Werror   if impl(ghc >= 6.12)     ghc-options:    -fwarn-dodgy-exports                     -fwarn-wrong-do-bind@@ -441,7 +442,7 @@   hs-source-dirs: src/main   main-is:        Main.hs   build-depends:-    Agda == 2.4.2.1+    Agda == 2.4.2.2     -- Nothing is used from the following package, except for the     -- prelude.     , base >= 3 && < 6

@@ -1,4 +1,22 @@ ------------------------------------------------------------------------+-- Release notes for Agda version 2.4.2.2+------------------------------------------------------------------------++Important changes since 2.4.2.1:++Bug fixes+=========++* Compilation on Windows fixed.++* Other issues fixed ( see https://code.google.com/p/agda/issues )+  1332+  1353+  1360+  1366+  1369++------------------------------------------------------------------------ -- Release notes for Agda version 2.4.2.1 ------------------------------------------------------------------------ @@ -62,11 +80,11 @@    Even though this code looks right, Agda complains about the type   expression `∀ u → unit ≡ dx u`.  If you ask Agda what should go-  there instead, she happily tells you that she wants-  `∀ u → unit ≡ dx u`.  Women!  In fact what you do not see and she+  there instead, it happily tells you that it wants+  `∀ u → unit ≡ dx u`. In fact what you do not see and Agda   will never show you is that the two expressions actually differ in   the invisible first argument to `dx`, which is visible only outside-  module `M`.  What she wants is an invisible `unit` after `dx`, but all+  module `M`.  What Agda wants is an invisible `unit` after `dx`, but all   you can write is an invisible `x` (which is inserted behind the   scenes). @@ -155,7 +173,7 @@   constructor applied to call argument, which is valid descent.    Note however, that Agda only looks for syntactic equality when-  identifying subterms, since she is not allowed to normalize terms on+  identifying subterms, since it is not allowed to normalize terms on   the rhs during termination checking.    Actually writing the dot pattern has no effect, this works as well,

@@ -10,7 +10,7 @@  ;;; Code: -(defvar agda2-version "2.4.2.1"+(defvar agda2-version "2.4.2.2"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.") 

@@ -10,6 +10,8 @@ import Control.Monad.State import Control.Monad.Reader +import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap import Data.List import Data.Map (Map) import qualified Data.Map as Map@@ -219,7 +221,7 @@             _         -> __IMPOSSIBLE__         case Map.toList eqs of             (c, Same n) : _ -> do-                let grp = eqGroups tags !!!! n+                let grp = fromMaybe __IMPOSSIBLE__ $ IntMap.lookup n $ eqGroups tags                 tag <- assignConstrTag' c (Set.toList grp)                 updateTags . fromMaybe __IMPOSSIBLE__ =<< setTag n tag tags { constrGroup = eqs }             _              -> return ()@@ -334,13 +336,13 @@   deriving Eq  data Tags = Tags-    { eqGroups    :: Map Int (Set QName)+    { eqGroups    :: IntMap (Set QName)     , constrGroup :: Map QName TagEq     }  initialTags :: Map QName Tag -> [QName] -> Tags initialTags setTags newNames = Tags-    { eqGroups    = Map.fromList $ zip [0..] (map Set.singleton newNames)+    { eqGroups    = IntMap.fromList $ zip [0..] (map Set.singleton newNames)     , constrGroup = Map.map IsTag setTags `Map.union` Map.fromList (zip newNames (map Same [0..]))     } @@ -358,19 +360,21 @@  setTag :: Int -> Tag -> Tags -> Compile TCM (Maybe Tags) setTag gid tag ts = return $ Just $ ts-    { constrGroup = foldr (\c -> Map.insert c (IsTag tag)) (constrGroup ts) (Set.toList $ eqGroups ts !!!! gid)}+    { constrGroup = foldr (\ c -> Map.insert c (IsTag tag))+                          (constrGroup ts)+                          (Set.toList $ fromMaybe __IMPOSSIBLE__ $ IntMap.lookup gid $ eqGroups ts) }  mergeGroups :: Int -> Int -> Tags -> Compile TCM (Maybe Tags) mergeGroups n1 n2 ts = do-    let g1s = eqGroups ts !!!! n1-        g2s = eqGroups ts !!!! n2+    let g1s = fromMaybe __IMPOSSIBLE__ $ IntMap.lookup n1 $ eqGroups ts+        g2s = fromMaybe __IMPOSSIBLE__ $ IntMap.lookup n2 $ eqGroups ts         gs  = Set.union g1s g2s         g1l = Set.toList g1s         g2l = Set.toList g2s     ifNotM (andM $ zipWith unifiable g1l g2l)         (return Nothing) $         return $ Just $ ts-            { eqGroups    = Map.delete n2 $ Map.insert n1 gs (eqGroups ts)+            { eqGroups    = IntMap.delete n2 $ IntMap.insert n1 gs (eqGroups ts)             , constrGroup = Map.fromList [ (e2, Same n1) | e2 <- g2l ] `Map.union` constrGroup ts             } 

@@ -25,7 +25,7 @@     mnameToList, qnameName, qnameModule, isInModule, nameId ) import Agda.Syntax.Internal   ( Name, Args, Type,-    Clause, Pattern(VarP,DotP,LitP,ConP,ProjP),+    Clause, Pattern, Pattern'(VarP,DotP,LitP,ConP,ProjP),     ClauseBodyF(Body,NoBody,Bind),ClauseBody,     Term(Var,Lam,Lit,Level,Def,Con,Pi,Sort,MetaV,DontCare,Shared,ExtLam),     unSpine, allApplyElims,

@@ -99,12 +99,24 @@         TP.text "give: instantiated meta type =" TP.<+> prettyTCM t'       v <- checkExpr e t'       case mvInstantiation mv of-        InstV _ v' -> unlessM ((Irrelevant ==) <$> asks envRelevance) $ do+        InstV xs v' -> unlessM ((Irrelevant ==) <$> asks envRelevance) $ do           reportSDoc "interaction.give" 20 $ TP.sep             [ TP.text "meta was already set to value v' = " TP.<+> prettyTCM v'+              TP.<+> TP.text " with free variables " TP.<+> return (fsep $ map pretty xs)             , TP.text "now comparing it to given value v = " TP.<+> prettyTCM v+            , TP.text "in context " TP.<+> inTopContext (prettyTCM ctx)             ]-          equalTerm t' v v'  -- Note: v' lives in context of meta+          -- The number of free variables should be at least the size of the context+          -- (Ideally, if we implemented contextual type theory, it should be the same.)+          when (length xs < size ctx) __IMPOSSIBLE__+          -- if there are more free variables than the context has+          -- we need to abstract over the additional ones (xs2)+          let (_xs1, xs2) = splitAt (size ctx) xs+          v' <- return $ foldr (\ (Arg ai x) -> I.Lam ai . I.Abs x) v' xs2+          reportSDoc "interaction.give" 20 $ TP.sep+            [ TP.text "in meta context, v' = " TP.<+> prettyTCM v'+            ]+          equalTerm t' v v'  -- Note: v' now lives in context of meta         _ -> updateMeta mi v       reify v 

@@ -325,17 +325,24 @@ --     This also meshes well with the fact that values (i.e. --     the arguments we are matching with) use @QName@. ---data Pattern-  = VarP PatVarName-    -- ^ The @PatVarName@ is a name suggestion.+data Pattern' x+  = VarP x+    -- ^ @x@   | DotP Term-  | ConP ConHead ConPatternInfo [NamedArg Pattern]-    -- ^ The @Pattern@s do not contain any projection copatterns.+    -- ^ @.t@+  | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]+    -- ^ @c ps@+    --   The subpatterns do not contain any projection copatterns.   | LitP Literal+    -- ^ E.g. @5@, @"hello"@.   | ProjP QName     -- ^ Projection copattern.  Can only appear by itself.-  deriving (Typeable, Show)+  deriving (Typeable, Show, Functor, Foldable, Traversable) +type Pattern = Pattern' PatVarName+    -- ^ The @PatVarName@ is a name suggestion.++ namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern namedVarP x = Named named $ VarP x   where named = if isUnderscore x then Nothing else Just $ unranged x@@ -937,4 +944,3 @@       NotHidden -> prettyPrec p       Hidden    -> braces . pretty       Instance  -> braces . braces . pretty-

@@ -1,6 +1,12 @@-{-# LANGUAGE CPP                  #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE OverlappingInstances   #-}+{-# LANGUAGE TupleSections          #-}+{-# LANGUAGE TypeSynonymInstances   #-}+{-# LANGUAGE UndecidableInstances   #-}  -- because of func. deps.  module Agda.Syntax.Internal.Pattern where @@ -57,55 +63,75 @@  -- * Tools for patterns -instance IsProjP Pattern where-  isProjP (ProjP d) = Just d-  isProjP _         = Nothing+-- | Label the pattern variables from left to right+--   using one label for each variable pattern and one for each dot pattern.+class LabelPatVars a b i | b -> i where+  labelPatVars :: a -> State [i] b+  -- ^ Intended, but unpractical due to the absence of type-level lambda, is:+  --   @labelPatVars :: f (Pattern' x) -> State [i] (f (Pattern' (i,x)))@ --- Special case of Agda.Syntax.Abstract.IsProjP (Arg...)--- instance IsProjP (Common.Arg c Pattern) where---   isProjP = isProjP . unArg+instance LabelPatVars a b i => LabelPatVars (Arg c a) (Arg c b) i where+  labelPatVars = traverse labelPatVars -{- NOTE: The following definition does not work, since Elim' already-   contains Arg.  Otherwise, we could have fixed it using traverseF.+instance LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i where+  labelPatVars = traverse labelPatVars -patternsToElims :: Permutation -> [I.NamedArg Pattern] -> Elims-patternsToElims perm aps = evalState (argPatsToElims aps) xs-  where-    xs   = permute (invertP __IMPOSSIBLE__ perm) $ downFrom (size perm)+instance LabelPatVars a b i => LabelPatVars [a] [b] i where+  labelPatVars = traverse labelPatVars -    tick :: State [Int] Int-    tick = do x : xs <- get; put xs; return x+instance LabelPatVars (Pattern' x) (Pattern' (i,x)) i where+  labelPatVars p =+    case p of+      VarP x       -> VarP . (,x) <$> next+      DotP t       -> DotP t <$ next+      ConP c mt ps -> ConP c mt <$> labelPatVars ps+      LitP l       -> return $ LitP l+      ProjP q      -> return $ ProjP q+    where next = do (x:xs) <- get; put xs; return x -    argPatsToElims :: [I.NamedArg Pattern] -> State [Int] Elims-    argPatsToElims = traverse $ traverse $ patToElim . namedThing+-- | Augment pattern variables with their de Bruijn index.+{-# SPECIALIZE numberPatVars :: Permutation -> [NamedArg (Pattern' x)] -> [(NamedArg (Pattern' (Int, x)))] #-}+numberPatVars :: LabelPatVars a b Int => Permutation -> a -> b+numberPatVars perm ps = evalState (labelPatVars ps) $+  permute (invertP __IMPOSSIBLE__ perm) $ downFrom $ size perm -    patToElim :: Pattern -> State [Int] (Elim' Term)-    patToElim p = case p of-      VarP _      -> Apply . flip var <$> tick-      DotP v      -> Apply v <$ tick   -- dot patterns count as variables-      ConP c _ ps -> Apply . Con c . map argFromElim <$> argPatsToElims ps-      LitP l      -> pure $ Apply $ Lit l-      ProjP d     -> pure $ Proj d--}+instance IsProjP Pattern where+  isProjP (ProjP d) = Just d+  isProjP _         = Nothing  patternsToElims :: Permutation -> [I.NamedArg Pattern] -> [Elim]-patternsToElims perm ps = evalState (mapM build' ps) xs+patternsToElims perm ps = map build' $ numberPatVars perm ps   where-    xs   = permute (invertP __IMPOSSIBLE__ perm) $ downFrom (size perm) -    tick :: State [Int] Int-    tick = do x : xs <- get; put xs; return x--    build' :: NamedArg Pattern -> State [Int] Elim+    build' :: NamedArg (Pattern' (Int, PatVarName)) -> Elim     build' = build . fmap namedThing -    build :: I.Arg Pattern -> State [Int] Elim-    build (Arg ai (VarP _)     ) = Apply . Arg ai . var <$> tick-    build (Arg ai (ConP c _ ps)) =-      Apply . Arg ai . Con c <$> mapM (argFromElim <.> build') ps-    build (Arg ai (DotP t)     ) = Apply (Arg ai t) <$ tick-    build (Arg ai (LitP l)     ) = return $ Apply $ Arg ai $ Lit l-    build (Arg ai (ProjP dest) ) = return $ Proj  $ dest+    build :: I.Arg (Pattern' (Int, PatVarName)) -> Elim+    build (Arg ai (VarP (i, _))) = Apply $ Arg ai $ var i+    build (Arg ai (ConP c _ ps)) = Apply $ Arg ai $ Con c $+      map (argFromElim . build') ps+    build (Arg ai (DotP t)     ) = Apply $ Arg ai t+    build (Arg ai (LitP l)     ) = Apply $ Arg ai $ Lit l+    build (Arg ai (ProjP dest) ) = Proj  $ dest++-- patternsToElims :: Permutation -> [I.NamedArg Pattern] -> [Elim]+-- patternsToElims perm ps = evalState (mapM build' ps) xs+--   where+--     xs   = permute (invertP __IMPOSSIBLE__ perm) $ downFrom (size perm)++--     tick :: State [Int] Int+--     tick = do x : xs <- get; put xs; return x++--     build' :: NamedArg Pattern -> State [Int] Elim+--     build' = build . fmap namedThing++--     build :: I.Arg Pattern -> State [Int] Elim+--     build (Arg ai (VarP _)     ) = Apply . Arg ai . var <$> tick+--     build (Arg ai (ConP c _ ps)) =+--       Apply . Arg ai . Con c <$> mapM (argFromElim <.> build') ps+--     build (Arg ai (DotP t)     ) = Apply (Arg ai t) <$ tick+--     build (Arg ai (LitP l)     ) = return $ Apply $ Arg ai $ Lit l+--     build (Arg ai (ProjP dest) ) = return $ Proj  $ dest  -- * One hole patterns 

@@ -32,6 +32,7 @@ import Agda.Utils.Graph.AdjacencyMap.Unidirectional as UtilGraphUni (tests) import Agda.Utils.List                        as UtilList   (tests) import Agda.Utils.PartialOrd                  as UtilPOrd   (tests)+import Agda.Utils.Permutation.Tests           as UtilPerm   (tests) import Agda.Utils.Warshall                    as UtilWarsh  (tests)  testSuite :: IO Bool@@ -39,6 +40,7 @@   [ Irrel.tests   , SizedTypes.tests   , UtilFav.tests+  , UtilPerm.tests   , UtilPOrd.tests   , CompEnco.tests   , InteEmac.tests

@@ -56,7 +56,7 @@   abstractTerm :: Term -> a -> a  instance AbstractTerm Term where-  abstractTerm u v | Just es <- u `isPrefixOf` v = Var 0 es+  abstractTerm u v | Just es <- u `isPrefixOf` v = Var 0 $ raise 1 es                    | otherwise                   =     case v of -- Andreas, 2013-10-20: the original impl. works only at base types

@@ -177,11 +177,24 @@ -}  checkSpine :: Type -> Term -> Elims -> Type -> TCM ()-checkSpine a self es t = inferSpine a self es >>= (`subtype` t)+checkSpine a self es t = do+  reportSDoc "tc.check.internal" 20 $ sep+    [ text "checking spine "+    , text "("+    , prettyTCM self+    , text " : "+    , prettyTCM a+    , text ")"+    , prettyTCM es+    , text " : "+    , prettyTCM t+    ]+  inferSpine a self es >>= (`subtype` t)  checkArgs :: Type -> Term -> Args -> Type -> TCM () checkArgs a self vs t = checkSpine a self (map Apply vs) t +-- | @checkArgInfo actual expected@. checkArgInfo :: I.ArgInfo -> I.ArgInfo -> TCM () checkArgInfo ai ai' = do   checkHiding    (getHiding ai)     (getHiding ai')

@@ -1,3 +1,5 @@+{-# OPTIONS_GHC -fwarn-unused-imports #-}+ {-# LANGUAGE CPP              #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternGuards    #-}@@ -42,9 +44,8 @@  import Agda.TypeChecking.Rules.LHS.Problem (FlexibleVar(..),flexibleVarFromHiding) import Agda.TypeChecking.Rules.LHS.Unify-import Agda.TypeChecking.Rules.LHS.Instantiate-import Agda.TypeChecking.Rules.LHS-import qualified Agda.TypeChecking.Rules.LHS.Split as Split+import Agda.TypeChecking.Rules.LHS.Instantiate (instantiateTel)+import Agda.TypeChecking.Rules.LHS (instantiatePattern)  import Agda.TypeChecking.Coverage.Match import Agda.TypeChecking.Coverage.SplitTree

@@ -211,7 +211,7 @@           -- The clause might not give as many patterns as there           -- are arguments (point-free style definitions).           let args' = take (length margs) args-          compareElims pol ftype org margs args'+          compareElims pol ftype (Def f []) margs args' {- Andreas, 2011-05-09 allow unsolved constraints as long as progress           unless (null cs) $ do             reportSDoc "tc.inj.invert" 30 $

@@ -205,7 +205,7 @@  -- | Record information that an argument is unused in 'Relevance'. mkUnused :: Relevance -> Relevance-mkUnused Relevant = UnusedArg   -- commenting out this line switches of 'UnusedArg' polarity machinery+mkUnused Relevant = UnusedArg   -- commenting out this line switches off 'UnusedArg' polarity machinery mkUnused r        = r  -- 'Irrelevant' is more informative than 'UnusedArg'.  -- | Improve 'Relevance' information in a type by polarity information.

@@ -227,363 +227,3 @@ quoteType v = do   kit <- quotingKit   runReduceM (quoteTypeWithKit kit v)--agdaTermType :: TCM Type-agdaTermType = El (mkType 0) <$> primAgdaTerm--qNameType :: TCM Type-qNameType = El (mkType 0) <$> primQName--type UnquoteM = ExceptionT UnquoteError TCM--runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError a)-runUnquoteM = runExceptionT--isCon :: ConHead -> TCM Term -> UnquoteM Bool-isCon con tm = do t <- lift tm-                  case ignoreSharing t of-                    Con con' _ -> return (con == con')-                    _ -> return False--{-unquoteFailedGeneric :: String -> UnquoteM a-unquoteFailedGeneric msg = typeError . GenericError $ "Unable to unquote the " ++ msg--unquoteFailed :: String -> String -> Term -> TCM a-unquoteFailed kind msg t = do doc <- prettyTCM t-                              unquoteFailedGeneric $ "term (" ++ show doc ++ ") of type " ++ kind ++ ".\nReason: " ++ msg ++ "."--}-class Unquote a where-  unquote :: Term -> UnquoteM a--unquoteH :: Unquote a => I.Arg Term -> UnquoteM a-unquoteH a | isHidden a && isRelevant a =-    unquote $ unArg a-unquoteH a = throwException $ BadVisibility "hidden"  a--unquoteN :: Unquote a => I.Arg Term -> UnquoteM a-unquoteN a | notHidden a && isRelevant a =-    unquote $ unArg a-unquoteN a = throwException $ BadVisibility "visible" a--choice :: Monad m => [(m Bool, m a)] -> m a -> m a-choice [] dflt = dflt-choice ((mb, mx) : mxs) dflt = ifM mb mx $ choice mxs dflt--ensureDef :: QName -> UnquoteM QName-ensureDef x = do-  i <- (theDef <$> getConstInfo x) `catchError` \_ -> return Axiom  -- for recursive unquoteDecl-  case i of-    Constructor{} -> do-      def <- lift $ prettyTCM =<< primAgdaTermDef-      con <- lift $ prettyTCM =<< primAgdaTermCon-      throwException $ ConInsteadOfDef x (show def) (show con)-    _ -> return x--ensureCon :: QName -> UnquoteM QName-ensureCon x = do-  i <- (theDef <$> getConstInfo x) `catchError` \_ -> return Axiom  -- for recursive unquoteDecl-  case i of-    Constructor{} -> return x-    _ -> do-      def <- lift $ prettyTCM =<< primAgdaTermDef-      con <- lift $ prettyTCM =<< primAgdaTermCon-      throwException $ DefInsteadOfCon x (show def) (show con)--pickName :: Type -> String-pickName a =-  case unEl a of-    Pi{}   -> "f"-    Sort{} -> "A"-    Def d _ | c:_ <- show (qnameName d),-              isAlpha c -> [toLower c]-    _    -> "_"--instance Unquote I.ArgInfo where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [h,r] -> do-        choice-          [(c `isCon` primArgArgInfo, ArgInfo <$> unquoteN h <*> unquoteN r <*> return [])]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "ArgInfo" t--instance Unquote a => Unquote (I.Arg a) where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [info,x] -> do-        choice-          [(c `isCon` primArgArg, Arg <$> unquoteN info <*> unquoteN x)]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Arg" t---- Andreas, 2013-10-20: currently, post-fix projections are not part of the--- quoted syntax.-instance Unquote a => Unquote (Elim' a) where-  unquote t = Apply <$> unquote t--instance Unquote Integer where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Lit (LitInt _ n) -> return n-      _ -> throwException $ NotALiteral "Integer" t--instance Unquote Double where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Lit (LitFloat _ x) -> return x-      _ -> throwException $ NotALiteral "Float" t--instance Unquote Char where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Lit (LitChar _ x) -> return x-      _ -> throwException $ NotALiteral "Char" t--instance Unquote Str where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Lit (LitString _ x) -> return (Str x)-      _ -> throwException $ NotALiteral "String" t--instance Unquote a => Unquote [a] where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [x,xs] -> do-        choice-          [(c `isCon` primCons, (:) <$> unquoteN x <*> unquoteN xs)]-          __IMPOSSIBLE__-      Con c [] -> do-        choice-          [(c `isCon` primNil, return [])]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "List" t--instance Unquote Hiding where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [] -> do-        choice-          [(c `isCon` primHidden,  return Hidden)-          ,(c `isCon` primInstance, return Instance)-          ,(c `isCon` primVisible, return NotHidden)]-          __IMPOSSIBLE__-      Con c vs -> __IMPOSSIBLE__-      _        -> throwException $ NotAConstructor "Hiding" t--instance Unquote Relevance where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [] -> do-        choice-          [(c `isCon` primRelevant,   return Relevant)-          ,(c `isCon` primIrrelevant, return Irrelevant)]-          __IMPOSSIBLE__-      Con c vs -> __IMPOSSIBLE__-      _        -> throwException $ NotAConstructor "Relevance" t--instance Unquote QName where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Lit (LitQName _ x) -> return x-      _                  -> throwException $ NotALiteral "QName" t--instance Unquote ConHead where-  unquote t = lift . getConHead =<< ensureCon =<< unquote t--instance Unquote a => Unquote (Abs a) where-  unquote t = Abs "_" <$> unquote t--instance Unquote Sort where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [] -> do-        choice-          [(c `isCon` primAgdaSortUnsupported, pure $ Type $ Max [Plus 0 $ UnreducedLevel $ hackReifyToMeta])]-          __IMPOSSIBLE__-      Con c [u] -> do-        choice-          [(c `isCon` primAgdaSortSet, Type <$> unquoteN u)-          ,(c `isCon` primAgdaSortLit, Type . levelMax . (:[]) . ClosedLevel <$> unquoteN u)]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Sort" t--instance Unquote Level where-  unquote l = Max . (:[]) . Plus 0 . UnreducedLevel <$> unquote l--instance Unquote Type where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [s, u] -> do-        choice-          [(c `isCon` primAgdaTypeEl, El <$> unquoteN s <*> unquoteN u)]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Type" t--instance Unquote Literal where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [x] ->-        choice-          [ (c `isCon` primAgdaLitNat,    LitInt    noRange <$> unquoteN x)-          , (c `isCon` primAgdaLitFloat,  LitFloat  noRange <$> unquoteN x)-          , (c `isCon` primAgdaLitChar,   LitChar   noRange <$> unquoteN x)-          , (c `isCon` primAgdaLitString, LitString noRange . unStr <$> unquoteN x)-          , (c `isCon` primAgdaLitQName,  LitQName  noRange <$> unquoteN x) ]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Literal" t--instance Unquote Term where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [] ->-        choice-          [(c `isCon` primAgdaTermUnsupported, pure hackReifyToMeta)]-          __IMPOSSIBLE__--      Con c [x] -> do-        choice-          [ (c `isCon` primAgdaTermSort,   Sort <$> unquoteN x)-          , (c `isCon` primAgdaTermLit,    Lit <$> unquoteN x) ]-          __IMPOSSIBLE__--      Con c [x, y] ->-        choice-          [ (c `isCon` primAgdaTermVar, Var <$> (fromInteger <$> unquoteN x) <*> unquoteN y)-          , (c `isCon` primAgdaTermCon, Con <$> unquoteN x <*> unquoteN y)-          , (c `isCon` primAgdaTermDef, Def <$> (ensureDef =<< unquoteN x) <*> unquoteN y)-          , (c `isCon` primAgdaTermLam, Lam <$> (flip setHiding defaultArgInfo <$> unquoteN x) <*> unquoteN y)-          , (c `isCon` primAgdaTermPi,  mkPi <$> (domFromArg <$> unquoteN x) <*> unquoteN y)-          , (c `isCon` primAgdaTermExtLam, mkExtLam <$> unquoteN x <*> unquoteN y) ]-          __IMPOSSIBLE__-        where-          mkExtLam = ExtLam-          mkPi a (Abs _ b) = Pi a (Abs x b)-            where x | 0 `freeIn` b = pickName (unDom a)-                    | otherwise    = "_"-          mkPi _ NoAbs{} = __IMPOSSIBLE__--      Con{} -> __IMPOSSIBLE__-      Lit{} -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Term" t--instance Unquote Pattern where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [] -> do-        choice-          [ (c `isCon` primAgdaPatVar,    pure (VarP "x"))-          , (c `isCon` primAgdaPatAbsurd, pure (VarP "()"))-          , (c `isCon` primAgdaPatDot,    pure (DotP hackReifyToMeta))-          ] __IMPOSSIBLE__-      Con c [x] -> do-        choice-          [ (c `isCon` primAgdaPatProj, ProjP <$> unquoteN x)-          , (c `isCon` primAgdaPatLit,  LitP  <$> unquoteN x) ]-          __IMPOSSIBLE__-      Con c [x, y] -> do-        choice-          [ (c `isCon` primAgdaPatCon, flip ConP Nothing <$> unquoteN x <*> (map (fmap unnamed) <$> unquoteN y)) ]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Pattern" t--data UnquotedFunDef = UnQFun Type [Clause]--instance Unquote Clause where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [x] -> do-        choice-          [ (c `isCon` primAgdaClauseAbsurd, mkClause Nothing <$> unquoteN x) ]-          __IMPOSSIBLE__-      Con c [x, y] -> do-        choice-          [ (c `isCon` primAgdaClauseClause, checkClause =<< mkClause . Just <$> unquoteN y <*> unquoteN x) ]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Clause" t-    where-      mkClause :: Maybe Term -> [I.Arg Pattern] -> I.Clause-      mkClause b ps0 =-        Clause { clauseRange     = noRange-               , clauseTel       = dummyTel n'-               , clausePerm      = Perm n vs-               , namedClausePats = ps-               , clauseBody      = mkBody n b-               , clauseType      = Nothing }-        where-          ps = map (fmap unnamed) ps0-          n  = vars True ps  -- with dot patterns-          n' = vars False ps -- without dot patterns-          dummyTel 0 = EmptyTel-          dummyTel n = ExtendTel (defaultDom typeDontCare) (Abs "x" $ dummyTel (n - 1))-          mkBody 0 b = maybe NoBody Body b-          mkBody n b = Bind $ Abs "x" $ mkBody (n - 1) b-          vars d ps = sum $ map (vars' d . namedArg) ps-          vars' d (ConP _ _ ps) = vars d ps-          vars' d VarP{}      = 1-          vars' d DotP{}      = if d then 1 else 0-          vars' d LitP{}      = 0-          vars' d ProjP{}     = 0--          vs = evalState (execWriterT $ mapM_ (computePerm . namedArg) ps) 0-          next = do n <- get; put (n + 1); return n--          computePerm (ConP _ _ ps) = mapM_ (computePerm . namedArg) ps-          computePerm VarP{}        = tell . (:[]) =<< next-          computePerm DotP{}        = () <$ next-          computePerm LitP{}        = return ()-          computePerm ProjP{}       = return ()--      checkClause :: I.Clause -> UnquoteM I.Clause-      checkClause cl@Clause{ clausePerm = Perm n vs , clauseBody = body } = do-        let freevs    = allVars $ freeVars $ fromMaybe __IMPOSSIBLE__ $ getBody body-            propervs  = Set.fromList $ map ((n-1)-) vs-            dottedvs  = Set.difference (Set.fromList [0..n-1]) propervs-            offending = Set.intersection freevs dottedvs-        Agda.TypeChecking.Monad.reportSDoc "tc.unquote.clause.dotvars" 30 $ vcat-          [ text $ "checkClause "-          , nest 2 $ text $ "free vars:      " ++ show freevs-          , nest 2 $ text $ "dotted vars:    " ++ show dottedvs-          , nest 2 $ text $ "offending vars: " ++ show offending-          ]-        if Set.null offending-          then return cl-          else throwException $ RhsUsesDottedVar (Set.toList offending) t--instance Unquote UnquotedFunDef where-  unquote t = do-    t <- lift $ reduce t-    case ignoreSharing t of-      Con c [x, y] -> do-        choice-          [ (c `isCon` primAgdaFunDefCon, UnQFun <$> unquoteN x <*> unquoteN y) ]-          __IMPOSSIBLE__-      Con c _ -> __IMPOSSIBLE__-      _ -> throwException $ NotAConstructor "Pattern" t--reifyUnquoted :: Reify a e => a -> TCM e-reifyUnquoted = nowReifyingUnquoted . disableDisplayForms . withShowAllArguments . reify-

@@ -938,6 +938,17 @@           (BlockedLevel m <$> instantiateFull' v)     UnreducedLevel v -> UnreducedLevel <$> instantiateFull' v +instance InstantiateFull Substitution where+  instantiateFull' sigma =+    case sigma of+      IdS                  -> return IdS+      EmptyS               -> return EmptyS+      Wk   n sigma         -> Wk   n         <$> instantiateFull' sigma+      Lift n sigma         -> Lift n         <$> instantiateFull' sigma+      Strengthen bot sigma -> Strengthen bot <$> instantiateFull' sigma+      t :# sigma           -> (:#) <$> instantiateFull' t+                                   <*> instantiateFull' sigma+ instance InstantiateFull Bool where     instantiateFull' = return 

@@ -30,8 +30,7 @@ import Agda.Syntax.Internal import Agda.TypeChecking.Monad hiding   ( enterClosure, underAbstraction_, underAbstraction, addCtx, mkContextEntry,-    isInstantiatedMeta, verboseS, reportSDoc, reportSLn, typeOfConst, lookupMeta,-    instantiateDef )+    isInstantiatedMeta, verboseS, reportSDoc, reportSLn, typeOfConst, lookupMeta ) import Agda.TypeChecking.Monad.Builtin hiding ( constructorForm ) import Agda.TypeChecking.Substitute import Agda.Interaction.Options

@@ -47,6 +47,7 @@ import Agda.TypeChecking.SizedTypes.Solve import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope+import Agda.TypeChecking.Unquote  import Agda.TypeChecking.Rules.Term import Agda.TypeChecking.Rules.Data    ( checkDataDef )

@@ -574,6 +574,10 @@   reportSLn "tc.with.top" 20 "created with display form"    -- Generate the type of the with function+  delta1 <- normalise delta1 -- Issue 1332: checkInternal is picky about argInfo+                             -- but module application is sloppy.+                             -- We normalise to get rid of Def's coming+                             -- from module applications.   candidateType <- withFunctionType delta1 vs as delta2 b   reportSDoc "tc.with.type" 10 $ sep [ text "candidate type:", nest 2 $ prettyTCM candidateType ]   reportSDoc "tc.with.type" 50 $ sep [ text "candidate type:", nest 2 $ text $ show candidateType ]

@@ -2,11 +2,13 @@  module Agda.TypeChecking.Rules.LHS where +import Prelude hiding (mapM)+ import Data.Maybe  import Control.Applicative-import Control.Monad-import Control.Monad.State+import Control.Monad hiding (mapM)+import Control.Monad.State hiding (mapM)  import Data.Traversable @@ -103,28 +105,60 @@          _           -> __IMPOSSIBLE__ -instantiatePattern :: Substitution -> Permutation -> [I.NamedArg Pattern] -> [I.NamedArg Pattern]++-- | In an internal pattern, replace some pattern variables+--   by dot patterns, according to the given substitution.+instantiatePattern+  :: Substitution+     -- ^ Partial substitution for the pattern variables,+     --   given in order of the clause telescope,+     --   (not in the order of occurrence in the patterns).+  -> Permutation+     -- ^ Map from the pattern variables to the telescope variables.+  -> [I.NamedArg Pattern]+     -- ^ Input patterns.+  -> [I.NamedArg Pattern]+     -- ^ Output patterns, with some @VarP@ replaced by @DotP@+     --   according to the @Substitution@. instantiatePattern sub perm ps-  | length sub /= length hps = error $ unlines [ "instantiatePattern:"-                                               , "  sub  = " ++ show sub-                                               , "  perm = " ++ show perm-                                               , "  ps   = " ++ show ps-                                               ]+  | length sub /= length hps = error $ unlines+      [ "instantiatePattern:"+      , "  sub  = " ++ show sub+      , "  perm = " ++ show perm+      , "  ps   = " ++ show ps+      ]   | otherwise  = foldr merge ps $ zipWith inst (reverse sub) hps   where+    -- For each pattern variable get a copy of the patterns+    -- focusing on this variable.+    -- Order them in the dependency (telescope) order.     hps = permute perm $ allHoles ps+    -- If we do not want to substitute a variable, we+    -- throw away the corresponding one-hole pattern.     inst Nothing  hps = Nothing+    -- If we want to substitute, we replace the variable+    -- by the dot pattern.     inst (Just t) hps = Just $ plugHole (DotP t) hps +    -- If we did not instantiate a variable, we can keep the original+    -- patterns in this iteration.     merge Nothing   ps = ps+    -- Otherwise, we merge the changes in @qs@ into @ps@.+    -- This means we walk simultaneously through @qs@ and @ps@+    -- and expect them to be the same everywhere except that+    -- a @q@ can be a @DotP@ and the corresponding @p@ a @VarP@.+    -- In this case, we take the @DotP@.+    -- Apparently, the other way round can also happen (why?).     merge (Just qs) ps = zipWith mergeA qs ps       where         mergeA a1 a2 = fmap (mergeP (namedArg a1) (namedArg a2) <$) a1         mergeP (DotP s)  (DotP t)           | s == t                    = DotP s           | otherwise                 = __IMPOSSIBLE__+        -- interesting cases:         mergeP (DotP t)  (VarP _)     = DotP t         mergeP (VarP _)  (DotP t)     = DotP t+        -- the rest is homomorphical         mergeP (DotP _)  _            = __IMPOSSIBLE__         mergeP _         (DotP _)     = __IMPOSSIBLE__         mergeP (ConP c1 mt1 ps) (ConP c2 mt2 qs)@@ -148,6 +182,41 @@         mergeP ProjP{} _              = __IMPOSSIBLE__         mergeP _       ProjP{}        = __IMPOSSIBLE__ ++-- | In an internal pattern, replace some pattern variables+--   by dot patterns, according to the given substitution.+instantiatePattern'+  :: Substitution+     -- ^ Partial substitution for the pattern variables,+     --   given in order of the clause telescope,+     --   (not in the order of occurrence in the patterns).+  -> Permutation+     -- ^ Map from the pattern variables to the telescope variables.+  -> [I.NamedArg Pattern]+     -- ^ Input patterns.+  -> [I.NamedArg Pattern]+     -- ^ Output patterns, with some @VarP@ replaced by @DotP@+     --   according to the @Substitution@.+instantiatePattern' sub perm ps = evalState (mapM goArg ps) 0+  where+    -- get a partial substitution from pattern variables to terms+    sub'    = inversePermute perm sub+    -- get next pattern variable+    next    = do n <- get; put (n+1); return n+    goArg   = traverse goNamed+    goNamed = traverse goPat+    goPat p = case p of+      VarP x       -> replace p+      DotP t       -> replace p+      ConP c mt ps -> ConP c mt <$> mapM goArg ps+      LitP{}       -> return p+      ProjP{}      -> return p+    replace p = do+      i <- next+      return $ fromMaybe p $ DotP <$> sub' !! i+++ -- | Check if a problem is solved. That is, if the patterns are all variables. isSolvedProblem :: Problem -> Bool isSolvedProblem problem = null (restPats $ problemRest problem) &&@@ -159,13 +228,6 @@     isSolved (A.ImplicitP _) = True     isSolved (A.AbsurdP _)   = True     isSolved _               = False-{--    isVar (A.VarP _)      = True-    isVar (A.WildP _)     = True-    isVar (A.ImplicitP _) = True-    isVar (A.AbsurdP _)   = True-    isVar _               = False--}  -- | For each user-defined pattern variable in the 'Problem', check -- that the corresponding data type (if any) does not contain a@@ -314,6 +376,16 @@   , lhsPermutation :: Permutation       -- ^ The permutation from pattern vars to @Δ@.   } +instance InstantiateFull LHSResult where+  instantiateFull' (LHSResult mtel tel sub xs ps t perm) = LHSResult+    <$> instantiateFull' mtel+    <*> instantiateFull' tel+    <*> instantiateFull' sub+    <*> return xs+    <*> instantiateFull' ps+    <*> instantiateFull' t+    <*> return perm+ -- | Check a LHS. Main function. -- --   @checkLeftHandSide a ps a ret@ checks that user patterns @ps@ eliminate@@ -370,10 +442,9 @@     mapM_ checkDotPattern dpi      let rho = renamingR perm -- I'm not certain about this...-        Perm n _ = perm-        xs  = [ stringToArgName $ "h" ++ show n | n <- [0..n - 1] ]-    applyRelevanceToContext (getRelevance b') $ do-      ret $ LHSResult mgamma delta rho xs qs b' perm+        xs  = [ stringToArgName $ "h" ++ show n | n <- [0..permRange perm - 1] ]+    lhsResult <- return $ LHSResult mgamma delta rho xs qs b' perm+    applyRelevanceToContext (getRelevance b') $ ret lhsResult  -- | The loop (tail-recursive): split at a variable in the problem until problem is solved checkLHS@@ -513,7 +584,9 @@       --   ]        -- Andreas 2010-09-07  propagate relevance info to new vars-      gamma' <- return $ fmap (applyRelevance $ argInfoRelevance info) gamma'+      -- Andreas 2014-11-25  clear 'Forced' and 'Unused'+      let updRel = ignoreForced . composeRelevance (getRelevance info)+      gamma' <- return $ mapRelevance updRel <$> gamma'        -- Insert implicit patterns       qs' <- insertImplicitPatterns ExpandLast qs gamma'

@@ -12,15 +12,19 @@  module Agda.TypeChecking.Rules.LHS.Unify where +import Prelude hiding (null)+ import Control.Arrow ((***)) import Control.Applicative hiding (empty) import Control.Monad.State import Control.Monad.Reader import Control.Monad.Writer (WriterT(..), MonadWriter(..), Monoid(..)) +import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap import Data.Map (Map) import qualified Data.Map as Map-import Data.List hiding (sort)+import Data.List hiding (null, sort)  import Data.Typeable (Typeable) import Data.Foldable (Foldable)@@ -41,7 +45,8 @@ import Agda.TypeChecking.DropArgs import Agda.TypeChecking.Level (reallyUnLevelView) import Agda.TypeChecking.Reduce-import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Pretty hiding (empty)+import qualified Agda.TypeChecking.Pretty as P import Agda.TypeChecking.Substitute hiding (Substitution) import qualified Agda.TypeChecking.Substitute as S import Agda.TypeChecking.Telescope@@ -60,8 +65,9 @@   )  import Agda.Utils.Maybe-import Agda.Utils.Size import Agda.Utils.Monad+import Agda.Utils.Null+import Agda.Utils.Size  #include "undefined.h" import Agda.Utils.Impossible@@ -83,6 +89,9 @@ instance HasConstInfo Unify where   getConstInfo = U . lift . lift . lift . lift . getConstInfo +-- UnifyEnv+------------------------------------------------------------------------+ data UnifyMayPostpone = MayPostpone | MayNotPostpone  type UnifyEnv = UnifyMayPostpone@@ -91,17 +100,14 @@ emptyUEnv = MayPostpone  noPostponing :: Unify a -> Unify a-noPostponing (U (ReaderT f)) = U . ReaderT . const $ f MayNotPostpone+noPostponing = U . local (const MayNotPostpone) . unUnify  askPostpone :: Unify UnifyMayPostpone-askPostpone = U . ReaderT $ return+askPostpone = U $ ask  -- | Output the result of unification (success or maybe). type UnifyOutput = Unifiable -emptyUOutput :: UnifyOutput-emptyUOutput = mempty- -- | Were two terms unifiable or did we have to postpone some equation such that we are not sure? data Unifiable   = Definitely  -- ^ Unification succeeded.@@ -127,7 +133,7 @@     Possibly ->   e  data Equality = Equal TypeHH Term Term-type Sub = Map Nat Term+type Sub = IntMap Term  data UnifyException   = ConstructorMismatch Type Term Term@@ -140,12 +146,13 @@   noMsg  = strMsg ""   strMsg = GenericUnifyException -data UnifyState = USt { uniSub    :: Sub-                      , uniConstr :: [Equality]-                      }+data UnifyState = USt+  { uniSub    :: Sub+  , uniConstr :: [Equality]+  }  emptyUState :: UnifyState-emptyUState = USt Map.empty []+emptyUState = USt IntMap.empty []  -- | Throw-away error message. projectionMismatch :: QName -> QName -> Unify a@@ -163,8 +170,8 @@   applySubst rho (Equal a s t) =     Equal (applySubst rho a) (applySubst rho s) (applySubst rho t) -onSub :: (Sub -> a) -> Unify a-onSub f = U $ gets $ f . uniSub+getSub :: Unify Sub+getSub = U $ gets uniSub  modSub :: (Sub -> Sub) -> Unify () modSub f = U $ modify $ \s -> s { uniSub = f $ uniSub s }@@ -253,19 +260,19 @@ i |-> (u, a) = do   occursCheck i u a   liftTCM $ reportSDoc "tc.lhs.unify.assign" 15 $ prettyTCM (var i) <+> text ":=" <+> prettyTCM u-  modSub $ Map.insert i (killRange u)+  modSub $ IntMap.insert i (killRange u)   -- Apply substitution to itself (issue 552)-  rho  <- onSub id+  rho  <- getSub   rho' <- traverse ureduce rho   modSub $ const rho'  makeSubstitution :: Sub -> S.Substitution makeSubstitution sub-  | Map.null sub = idS-  | otherwise    = map val [0 .. highestIndex] ++# raiseS (highestIndex + 1)+  | null sub  = idS+  | otherwise = map val [0 .. highestIndex] ++# raiseS (highestIndex + 1)   where-    highestIndex = fst $ Map.findMax sub-    val i = maybe (var i) id $ Map.lookup i sub+    highestIndex = fst $ IntMap.findMax sub+    val i = fromMaybe (var i) $ IntMap.lookup i sub  -- | Apply the current substitution on a term and reduce to weak head normal form. class UReduce t where@@ -273,7 +280,7 @@  instance UReduce Term where   ureduce u = doEtaContractImplicit $ do-    rho <- onSub makeSubstitution+    rho <- makeSubstitution <$> getSub -- Andreas, 2013-10-24 the following call to 'normalise' is problematic -- (see issue 924).  Instead, we only normalize if unifyAtomHH is undecided. --    liftTCM $ etaContract =<< normalise (applySubst rho u)@@ -338,11 +345,15 @@       where         Just u = s !! i +    -- @inst i u v@ replaces index @i@ in @v@ by @u@, without removing the index.     inst :: Nat -> Term -> Term -> Term     inst i u v = applySubst us v       where us = [var j | j <- [0..i - 1] ] ++# u :# raiseS (i + 1) -data UnificationResult = Unifies Substitution | NoUnify Type Term Term | DontKnow TCErr+data UnificationResult+  = Unifies Substitution+  | NoUnify Type Term Term+  | DontKnow TCErr  -- | Are we in a homogeneous (one type) or heterogeneous (two types) situation? data HomHet a@@ -491,7 +502,7 @@       Right _                               -> do         checkEqualities $ applySubst (makeSubstitution s) eqs         let n = maximum $ (-1) : flex'-        return $ Unifies $ flattenSubstitution [ Map.lookup i s | i <- [0..n] ]+        return $ Unifies $ flattenSubstitution [ IntMap.lookup i s | i <- [0..n] ]   `catchError` \err -> case err of      TypeError _ (Closure {clValue = WithoutKError{}}) -> throwError err      _                                                 -> return $ DontKnow err@@ -744,9 +755,9 @@        liftTCM $ reportSDoc "tc.lhs.unify" 15 $         sep [ text "unifyAtom"-            , nest 2 $ prettyTCM u <> if flexibleTerm u then text " (flexible)" else empty+            , nest 2 $ prettyTCM u <> if flexibleTerm u then text " (flexible)" else P.empty             , nest 2 $ text "=?="-            , nest 2 $ prettyTCM v <> if flexibleTerm v then text " (flexible)" else empty+            , nest 2 $ prettyTCM v <> if flexibleTerm v then text " (flexible)" else P.empty             , nest 2 $ text ":" <+> prettyTCM aHH             ]       liftTCM $ reportSDoc "tc.lhs.unify" 60 $

@@ -80,6 +80,8 @@       reportSDoc "tc.rec" 15 $ text "checking fields"       -- WRONG: contype <- workOnTypes $ killRange <$> (instantiateFull =<< isType_ contel)       contype <- killRange <$> (instantiateFull =<< isType_ contel)+      reportSDoc "tc.rec" 20 $ vcat+        [ text "contype = " <+> prettyTCM contype ]        -- compute the field telescope (does not include record parameters)       let TelV ftel _ = telView' contype@@ -97,6 +99,9 @@         Sort s  -> return s         _       -> typeError $ ShouldBeASort t0       gamma <- getContextTelescope  -- the record params (incl. module params)+      reportSDoc "tc.rec" 20 $ vcat+        [ text "gamma = " <+> inTopContext (prettyTCM gamma) ]+       -- record type (name applied to parameters)       let rect = El s $ Def name $ map Apply $ teleArgs gamma 

@@ -56,6 +56,7 @@ import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.TypeChecking.Rules.LHS (checkLeftHandSide, LHSResult(..))+import Agda.TypeChecking.Unquote  import {-# SOURCE #-} Agda.TypeChecking.Empty (isEmptyType) import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkSectionApplication)

@@ -20,7 +20,7 @@ import Agda.Utils.Size import Agda.Utils.Tuple import Agda.Utils.VarSet (VarSet)-import qualified Agda.Utils.VarSet as Set+import qualified Agda.Utils.VarSet as VarSet  #include "undefined.h" import Agda.Utils.Impossible@@ -113,24 +113,33 @@  -- | A telescope split in two. data SplitTel = SplitTel-      { firstPart  :: Telescope-      , secondPart :: Telescope-      , splitPerm  :: Permutation-      }+  { firstPart  :: Telescope+  , secondPart :: Telescope+  , splitPerm  :: Permutation+    -- ^ The permutation takes us from the original telescope to+    --   @firstPart ++ secondPart@.+  }  -- | Split a telescope into the part that defines the given variables and the --   part that doesn't.-splitTelescope :: VarSet -> Telescope -> SplitTel+--+--   See 'Agda.TypeChecking.Tests.prop_splitTelescope'.+splitTelescope+  :: VarSet     -- ^ A set of de Bruijn indices.+  -> Telescope  -- ^ Original telescope.+  -> SplitTel   -- ^ @firstPart@ mentions the given variables, @secondPart@ not. splitTelescope fv tel = SplitTel tel1 tel2 perm   where     names = teleNames tel     ts0   = flattenTel tel-     n     = size tel      -- We start with a rough split into fv and the rest. This will most likely     -- not be correct so we patch it up later with reorderTel.-    is    = map (n - 1 -) $ filter (< n) $ reverse $ Set.toList fv++    -- Convert given de Bruijn indices into ascending list of de Bruijn levels.+    is    = map (n - 1 -) $ dropWhile (>= n) $ VarSet.toDescList fv+    -- Compute the complement (de Bruijn levels not mentioned in @fv@).     isC   = [0..n - 1] \\ is     perm0 = Perm n $ is ++ isC @@ -146,9 +155,8 @@      tel'  = unflattenTel (permute perm names) ts2 -    Perm _ js = perm-    m         = genericLength $ takeWhile (`notElem` is) (reverse js)-    (tel1, tel2) = telFromList -*- telFromList $ genericSplitAt (n - m) $ telToList tel'+    m            = length $ takeWhile (`notElem` is) $ reverse $ permPicks perm+    (tel1, tel2) = telFromList -*- telFromList $ splitAt (n - m) $ telToList tel'  telView :: Type -> TCM TelView telView = telViewUpTo (-1)

@@ -0,0 +1,403 @@+{-# LANGUAGE CPP                  #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE PatternGuards        #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Agda.TypeChecking.Unquote where++import Control.Applicative+import Control.Monad.State (evalState, get, put)+import Control.Monad.Writer (execWriterT, tell)+import Control.Monad.Trans (lift)++import Data.Char+import Data.Maybe (fromMaybe)+import Data.Traversable (traverse)++import Agda.Syntax.Common+import Agda.Syntax.Internal as I+import Agda.Syntax.Literal+import Agda.Syntax.Position+import Agda.Syntax.Translation.InternalToAbstract++import Agda.TypeChecking.CompiledClause+import Agda.TypeChecking.Datatypes ( getConHead )+import Agda.TypeChecking.DropArgs+import Agda.TypeChecking.Free+import Agda.TypeChecking.Level+import Agda.TypeChecking.Monad+import Agda.TypeChecking.Monad.Builtin+import Agda.TypeChecking.Monad.Exception+import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Reduce+import Agda.TypeChecking.Reduce.Monad+import Agda.TypeChecking.Substitute++import Agda.Utils.Except+import Agda.Utils.Impossible+import Agda.Utils.Monad ( ifM )+import Agda.Utils.Permutation ( Permutation(Perm) )+import Agda.Utils.String ( Str(Str), unStr )+import Agda.Utils.VarSet (VarSet)+import qualified Agda.Utils.VarSet as Set++#include "undefined.h"++agdaTermType :: TCM Type+agdaTermType = El (mkType 0) <$> primAgdaTerm++qNameType :: TCM Type+qNameType = El (mkType 0) <$> primQName++type UnquoteM = ExceptionT UnquoteError TCM++runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError a)+runUnquoteM = runExceptionT++isCon :: ConHead -> TCM Term -> UnquoteM Bool+isCon con tm = do t <- lift tm+                  case ignoreSharing t of+                    Con con' _ -> return (con == con')+                    _ -> return False++{-unquoteFailedGeneric :: String -> UnquoteM a+unquoteFailedGeneric msg = typeError . GenericError $ "Unable to unquote the " ++ msg++unquoteFailed :: String -> String -> Term -> TCM a+unquoteFailed kind msg t = do doc <- prettyTCM t+                              unquoteFailedGeneric $ "term (" ++ show doc ++ ") of type " ++ kind ++ ".\nReason: " ++ msg ++ "."+-}+class Unquote a where+  unquote :: Term -> UnquoteM a++unquoteH :: Unquote a => I.Arg Term -> UnquoteM a+unquoteH a | isHidden a && isRelevant a =+    unquote $ unArg a+unquoteH a = throwException $ BadVisibility "hidden"  a++unquoteN :: Unquote a => I.Arg Term -> UnquoteM a+unquoteN a | notHidden a && isRelevant a =+    unquote $ unArg a+unquoteN a = throwException $ BadVisibility "visible" a++choice :: Monad m => [(m Bool, m a)] -> m a -> m a+choice [] dflt = dflt+choice ((mb, mx) : mxs) dflt = ifM mb mx $ choice mxs dflt++ensureDef :: QName -> UnquoteM QName+ensureDef x = do+  i <- (theDef <$> getConstInfo x) `catchError` \_ -> return Axiom  -- for recursive unquoteDecl+  case i of+    Constructor{} -> do+      def <- lift $ prettyTCM =<< primAgdaTermDef+      con <- lift $ prettyTCM =<< primAgdaTermCon+      throwException $ ConInsteadOfDef x (show def) (show con)+    _ -> return x++ensureCon :: QName -> UnquoteM QName+ensureCon x = do+  i <- (theDef <$> getConstInfo x) `catchError` \_ -> return Axiom  -- for recursive unquoteDecl+  case i of+    Constructor{} -> return x+    _ -> do+      def <- lift $ prettyTCM =<< primAgdaTermDef+      con <- lift $ prettyTCM =<< primAgdaTermCon+      throwException $ DefInsteadOfCon x (show def) (show con)++pickName :: Type -> String+pickName a =+  case unEl a of+    Pi{}   -> "f"+    Sort{} -> "A"+    Def d _ | c:_ <- show (qnameName d),+              isAlpha c -> [toLower c]+    _    -> "_"++instance Unquote I.ArgInfo where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [h,r] -> do+        choice+          [(c `isCon` primArgArgInfo, ArgInfo <$> unquoteN h <*> unquoteN r <*> return [])]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "ArgInfo" t++instance Unquote a => Unquote (I.Arg a) where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [info,x] -> do+        choice+          [(c `isCon` primArgArg, Arg <$> unquoteN info <*> unquoteN x)]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Arg" t++-- Andreas, 2013-10-20: currently, post-fix projections are not part of the+-- quoted syntax.+instance Unquote a => Unquote (Elim' a) where+  unquote t = Apply <$> unquote t++instance Unquote Integer where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Lit (LitInt _ n) -> return n+      _ -> throwException $ NotALiteral "Integer" t++instance Unquote Double where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Lit (LitFloat _ x) -> return x+      _ -> throwException $ NotALiteral "Float" t++instance Unquote Char where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Lit (LitChar _ x) -> return x+      _ -> throwException $ NotALiteral "Char" t++instance Unquote Str where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Lit (LitString _ x) -> return (Str x)+      _ -> throwException $ NotALiteral "String" t++instance Unquote a => Unquote [a] where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [x,xs] -> do+        choice+          [(c `isCon` primCons, (:) <$> unquoteN x <*> unquoteN xs)]+          __IMPOSSIBLE__+      Con c [] -> do+        choice+          [(c `isCon` primNil, return [])]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "List" t++instance Unquote Hiding where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [] -> do+        choice+          [(c `isCon` primHidden,  return Hidden)+          ,(c `isCon` primInstance, return Instance)+          ,(c `isCon` primVisible, return NotHidden)]+          __IMPOSSIBLE__+      Con c vs -> __IMPOSSIBLE__+      _        -> throwException $ NotAConstructor "Hiding" t++instance Unquote Relevance where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [] -> do+        choice+          [(c `isCon` primRelevant,   return Relevant)+          ,(c `isCon` primIrrelevant, return Irrelevant)]+          __IMPOSSIBLE__+      Con c vs -> __IMPOSSIBLE__+      _        -> throwException $ NotAConstructor "Relevance" t++instance Unquote QName where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Lit (LitQName _ x) -> return x+      _                  -> throwException $ NotALiteral "QName" t++instance Unquote ConHead where+  unquote t = lift . getConHead =<< ensureCon =<< unquote t++instance Unquote a => Unquote (Abs a) where+  unquote t = Abs "_" <$> unquote t++instance Unquote Sort where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [] -> do+        choice+          [(c `isCon` primAgdaSortUnsupported, pure $ Type $ Max [Plus 0 $ UnreducedLevel $ hackReifyToMeta])]+          __IMPOSSIBLE__+      Con c [u] -> do+        choice+          [(c `isCon` primAgdaSortSet, Type <$> unquoteN u)+          ,(c `isCon` primAgdaSortLit, Type . levelMax . (:[]) . ClosedLevel <$> unquoteN u)]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Sort" t++instance Unquote Level where+  unquote l = Max . (:[]) . Plus 0 . UnreducedLevel <$> unquote l++instance Unquote Type where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [s, u] -> do+        choice+          [(c `isCon` primAgdaTypeEl, El <$> unquoteN s <*> unquoteN u)]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Type" t++instance Unquote Literal where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [x] ->+        choice+          [ (c `isCon` primAgdaLitNat,    LitInt    noRange <$> unquoteN x)+          , (c `isCon` primAgdaLitFloat,  LitFloat  noRange <$> unquoteN x)+          , (c `isCon` primAgdaLitChar,   LitChar   noRange <$> unquoteN x)+          , (c `isCon` primAgdaLitString, LitString noRange . unStr <$> unquoteN x)+          , (c `isCon` primAgdaLitQName,  LitQName  noRange <$> unquoteN x) ]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Literal" t++instance Unquote Term where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [] ->+        choice+          [(c `isCon` primAgdaTermUnsupported, pure hackReifyToMeta)]+          __IMPOSSIBLE__++      Con c [x] -> do+        choice+          [ (c `isCon` primAgdaTermSort,   Sort <$> unquoteN x)+          , (c `isCon` primAgdaTermLit,    Lit <$> unquoteN x) ]+          __IMPOSSIBLE__++      Con c [x, y] ->+        choice+          [ (c `isCon` primAgdaTermVar, Var <$> (fromInteger <$> unquoteN x) <*> unquoteN y)+          , (c `isCon` primAgdaTermCon, Con <$> unquoteN x <*> unquoteN y)+          , (c `isCon` primAgdaTermDef, Def <$> (ensureDef =<< unquoteN x) <*> unquoteN y)+          , (c `isCon` primAgdaTermLam, Lam <$> (flip setHiding defaultArgInfo <$> unquoteN x) <*> unquoteN y)+          , (c `isCon` primAgdaTermPi,  mkPi <$> (domFromArg <$> unquoteN x) <*> unquoteN y)+          , (c `isCon` primAgdaTermExtLam, mkExtLam <$> unquoteN x <*> unquoteN y) ]+          __IMPOSSIBLE__+        where+          mkExtLam = ExtLam+          mkPi a (Abs _ b) = Pi a (Abs x b)+            where x | 0 `freeIn` b = pickName (unDom a)+                    | otherwise    = "_"+          mkPi _ NoAbs{} = __IMPOSSIBLE__++      Con{} -> __IMPOSSIBLE__+      Lit{} -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Term" t++instance Unquote Pattern where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [] -> do+        choice+          [ (c `isCon` primAgdaPatVar,    pure (VarP "x"))+          , (c `isCon` primAgdaPatAbsurd, pure (VarP "()"))+          , (c `isCon` primAgdaPatDot,    pure (DotP hackReifyToMeta))+          ] __IMPOSSIBLE__+      Con c [x] -> do+        choice+          [ (c `isCon` primAgdaPatProj, ProjP <$> unquoteN x)+          , (c `isCon` primAgdaPatLit,  LitP  <$> unquoteN x) ]+          __IMPOSSIBLE__+      Con c [x, y] -> do+        choice+          [ (c `isCon` primAgdaPatCon, flip ConP Nothing <$> unquoteN x <*> (map (fmap unnamed) <$> unquoteN y)) ]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Pattern" t++data UnquotedFunDef = UnQFun Type [Clause]++instance Unquote Clause where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [x] -> do+        choice+          [ (c `isCon` primAgdaClauseAbsurd, mkClause Nothing <$> unquoteN x) ]+          __IMPOSSIBLE__+      Con c [x, y] -> do+        choice+          [ (c `isCon` primAgdaClauseClause, checkClause =<< mkClause . Just <$> unquoteN y <*> unquoteN x) ]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Clause" t+    where+      mkClause :: Maybe Term -> [I.Arg Pattern] -> I.Clause+      mkClause b ps0 =+        Clause { clauseRange     = noRange+               , clauseTel       = dummyTel n'+               , clausePerm      = Perm n vs+               , namedClausePats = ps+               , clauseBody      = mkBody n b+               , clauseType      = Nothing }+        where+          ps = map (fmap unnamed) ps0+          n  = vars True ps  -- with dot patterns+          n' = vars False ps -- without dot patterns+          dummyTel 0 = EmptyTel+          dummyTel n = ExtendTel (defaultDom typeDontCare) (Abs "x" $ dummyTel (n - 1))+          mkBody 0 b = maybe NoBody Body b+          mkBody n b = Bind $ Abs "x" $ mkBody (n - 1) b+          vars d ps = sum $ map (vars' d . namedArg) ps+          vars' d (ConP _ _ ps) = vars d ps+          vars' d VarP{}      = 1+          vars' d DotP{}      = if d then 1 else 0+          vars' d LitP{}      = 0+          vars' d ProjP{}     = 0++          vs = evalState (execWriterT $ mapM_ (computePerm . namedArg) ps) 0+          next = do n <- get; put (n + 1); return n++          computePerm (ConP _ _ ps) = mapM_ (computePerm . namedArg) ps+          computePerm VarP{}        = tell . (:[]) =<< next+          computePerm DotP{}        = () <$ next+          computePerm LitP{}        = return ()+          computePerm ProjP{}       = return ()++      checkClause :: I.Clause -> UnquoteM I.Clause+      checkClause cl@Clause{ clausePerm = Perm n vs , clauseBody = body } = do+        let freevs    = allVars $ freeVars $ fromMaybe __IMPOSSIBLE__ $ getBody body+            propervs  = Set.fromList $ map ((n-1)-) vs+            dottedvs  = Set.difference (Set.fromList [0..n-1]) propervs+            offending = Set.intersection freevs dottedvs+        Agda.TypeChecking.Monad.reportSDoc "tc.unquote.clause.dotvars" 30 $ vcat+          [ text $ "checkClause "+          , nest 2 $ text $ "free vars:      " ++ show freevs+          , nest 2 $ text $ "dotted vars:    " ++ show dottedvs+          , nest 2 $ text $ "offending vars: " ++ show offending+          ]+        if Set.null offending+          then return cl+          else throwException $ RhsUsesDottedVar (Set.toList offending) t++instance Unquote UnquotedFunDef where+  unquote t = do+    t <- lift $ reduce t+    case ignoreSharing t of+      Con c [x, y] -> do+        choice+          [ (c `isCon` primAgdaFunDefCon, UnQFun <$> unquoteN x <*> unquoteN y) ]+          __IMPOSSIBLE__+      Con c _ -> __IMPOSSIBLE__+      _ -> throwException $ NotAConstructor "Pattern" t++reifyUnquoted :: Reify a e => a -> TCM e+reifyUnquoted = nowReifyingUnquoted . disableDisplayForms . withShowAllArguments . reify

@@ -76,7 +76,7 @@   | otherwise    = __IMPOSSIBLE__  #if mingw32_HOST_OS-prop_mkAbsolute :: FilePath -> Propertty+prop_mkAbsolute :: FilePath -> Property #else prop_mkAbsolute :: FilePath -> Bool #endif

@@ -3,11 +3,16 @@ {-# LANGUAGE DeriveFoldable     #-} {-# LANGUAGE DeriveFunctor      #-} {-# LANGUAGE DeriveTraversable  #-}+{-# LANGUAGE FlexibleInstances  #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TupleSections      #-}  module Agda.Utils.Permutation where  import Prelude hiding (drop) +import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap import Data.List hiding (drop) import qualified Data.List as List import Data.Maybe@@ -16,8 +21,9 @@ import Data.Traversable (Traversable) import Data.Typeable (Typeable) -import Agda.Utils.Size+import Agda.Utils.Functor import Agda.Utils.List ((!!!))+import Agda.Utils.Size  #include "undefined.h" import Agda.Utils.Impossible@@ -63,6 +69,33 @@     xs !!!! n | n < 0     = Nothing               | otherwise = xs !!! n +-- |  Invert a Permutation on a partial finite int map.+-- @inversePermute perm f = f'@+-- such that @permute perm f' = f@+--+-- Example, with map represented as @[Maybe a]@:+-- @+--   f    = [Nothing, Just a, Just b ]+--   perm = Perm 4 [3,0,2]+--   f'   = [ Just a , Nothing , Just b , Nothing ]+-- @+-- Zipping @perm@ with @f@ gives @[(0,a),(2,b)]@, after compression+-- with @catMaybes@.  This is an @IntMap@ which can easily+-- written out into a substitution again.++class InversePermute a b where+  inversePermute :: Permutation -> a -> b++instance InversePermute [Maybe a] [(Int,a)] where+  inversePermute (Perm n is) = catMaybes . zipWith (\ i ma -> (i,) <$> ma) is++instance InversePermute [Maybe a] (IntMap a) where+  inversePermute p = IntMap.fromList . inversePermute p++instance InversePermute [Maybe a] [Maybe a] where+  inversePermute p@(Perm n _) = tabulate . inversePermute p+    where tabulate m = for [0..n-1] $ \ i -> IntMap.lookup i m+ -- | Identity permutation. idP :: Int -> Permutation idP n = Perm n [0..n - 1]@@ -159,7 +192,9 @@         xs = [ x | (x, []) <- g ]         remove x g = [ (y, filter (/= x) ys) | (y, ys) <- g, x /= y ] +------------------------------------------------------------------------ -- * Drop (apply) and undrop (abstract)+------------------------------------------------------------------------  -- | Delayed dropping which allows undropping. data Drop a = Drop@@ -189,3 +224,7 @@     Perm (n + m) $ [0..m-1] ++ map (+ m) (List.drop k xs)     where m = -k   unDrop m = dropMore (-m) -- allow picking up more than dropped++------------------------------------------------------------------------+-- * Properties, see 'Agda.Utils.Permutation.Tests'+------------------------------------------------------------------------

@@ -0,0 +1,117 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}++{-# LANGUAGE CPP                #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable     #-}+{-# LANGUAGE DeriveFunctor      #-}+{-# LANGUAGE DeriveTraversable  #-}+{-# LANGUAGE TemplateHaskell    #-}++module Agda.Utils.Permutation.Tests (tests) where++import Data.Functor+import Data.List as List+import Data.Maybe++import Test.QuickCheck+import Test.QuickCheck.All++import Agda.Utils.Permutation++------------------------------------------------------------------------+-- * Properties+------------------------------------------------------------------------++instance Arbitrary Permutation where+  arbitrary = do+    is <- nub . map getNonNegative <$> arbitrary+    NonNegative n <- arbitrary+    return $ Perm (if null is then n else maximum is + n + 1) is++data ComposablePermutations = ComposablePermutations Permutation Permutation+  deriving (Eq, Show)++instance Arbitrary ComposablePermutations where+  arbitrary = do+    p2@(Perm n is) <- arbitrary+    let m = length is+    p1 <- Perm m . filter (< m) . map getNonNegative <$> arbitrary+    return $ ComposablePermutations p1 p2++type A = Int++-- | Extend a list by indefinitely many elements.+withStream :: Testable b+  => ([a] -> b)  -- ^ Stream function.+  -> [a]         -- ^ Initial segment.+  -> a           -- ^ Default element, appended ad infinitum.+  -> b+withStream k as a = k $ as ++ repeat a++-- | Apply a permutation to a list which might be too short.+--   Silently discard picks that go beyond the list's boundaries.+permutePartial :: Permutation -> [a] -> [a]+permutePartial perm xs =+  catMaybes $ permute perm $ map Just xs ++ repeat Nothing+  -- Note: we have to add @Nothing@s to make @permute@ total.++-- | @perm([0..n-1]) == perm@+prop_permute_id_r :: Permutation -> Bool+prop_permute_id_r perm@(Perm n picks) =+  permute perm [0..] == picks++-- | @idP(xs) == xs@+prop_permute_id_l :: Int -> [A] -> A -> Bool+prop_permute_id_l n = withStream $ \ xs ->+  permute (idP n) xs == take n xs++-- | @takeP n perm = perm . take n@+prop_takeP :: Int -> Permutation -> [A] -> A -> Bool+prop_takeP n perm = withStream $ \ xs ->+  permute (takeP n perm) xs == permutePartial perm (take n xs)+  -- Note: we have to add @Nothing@s to make @permute@ total.++-- | @(droppedP perm)(xs) = xs \\ perm(xs)@+prop_droppedP :: Permutation -> [A] -> A -> Bool+prop_droppedP perm@(Perm n _) = withStream $ \ xs -> let xs' = take n xs in+  sort (permute (droppedP perm) xs') == sort (xs' \\ permute perm xs')++-- | @(p1 ∘ p2)(xs) = p1(p2(xs))@+prop_composeP :: ComposablePermutations -> [A] -> A -> Bool+prop_composeP (ComposablePermutations p1 p2) = withStream $ \ xs ->+  permute (composeP p1 p2) xs == permutePartial p1 (permute p2 xs)++-- | @p ∘ p⁻¹ ∘ p = p@+prop_invertP_left :: Permutation -> Int -> [A] -> A -> Bool+prop_invertP_left p err = withStream $ \ xs -> let ys = permute p xs in+  permute p (permute (invertP err p) ys) == ys++-- NOT QUITE RIGHT YET:+-- -- | @p⁻1 ∘ p ∘ p⁻¹ = p⁻¹@+-- prop_invertP_right :: Permutation -> Int -> [A] -> A -> Bool+-- prop_invertP_right p err = withStream $ \ xs ->+--   let pinv = invertP err p+--       ys   = permute pinv xs+--   in  permute pinv (permute p ys) == ys++-- | @reverseP p = reverse . p . reverse@+prop_reverseP :: Permutation -> [A] -> A -> Bool+prop_reverseP p@(Perm n _) = withStream $ \ xs0 -> let xs = take n xs0 in+  permute (reverseP p) xs == reverse (permute p (reverse xs))++-- | @permute p . inversePermute p = id@+prop_inversePermute :: Permutation -> [Maybe A] -> Maybe A -> Bool+prop_inversePermute p@(Perm _ is) = withStream $ \ xs0 ->+  let xs = take (length is) xs0+      ys = inversePermute p xs+  in  permute p ys == xs++-- Template Haskell hack to make the following $quickCheckAll work+-- under ghc-7.8.+return [] -- KEEP!++-- | All tests as collected by 'quickCheckAll'.+tests :: IO Bool+tests = do+  putStrLn "Agda.Utils.Permutation"+  $quickCheckAll

@@ -1,18 +1,29 @@+{-# LANGUAGE CPP #-}+ -- | Var field implementation of sets of (small) natural numbers.+ module Agda.Utils.VarSet   ( VarSet-  , union, unions, member, empty, delete, singleton, fromList, toList, isSubsetOf, Set.null+  , union, unions, member, empty, delete, singleton+  , fromList, toList, toDescList+  , isSubsetOf, IntSet.null   , intersection, difference   , Agda.Utils.VarSet.subtract   )   where -import Data.IntSet as Set+import Data.IntSet (IntSet)+import Data.IntSet as IntSet -type VarSet = Set.IntSet+type VarSet = IntSet  subtract :: Int -> VarSet -> VarSet-subtract n s = Set.map (Prelude.subtract n) s+subtract n = IntSet.map (Prelude.subtract n)++#if !MIN_VERSION_containers(0,5,0)+toDescList :: VarSet -> [Int]+toDescList = reverse . toList+#endif  {- import Data.Bits