diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -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 diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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, diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el --- a/src/data/emacs-mode/agda2-mode.el +++ b/src/data/emacs-mode/agda2-mode.el @@ -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.") diff --git a/src/full/Agda/Compiler/Epic/Injection.hs b/src/full/Agda/Compiler/Epic/Injection.hs --- a/src/full/Agda/Compiler/Epic/Injection.hs +++ b/src/full/Agda/Compiler/Epic/Injection.hs @@ -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 } diff --git a/src/full/Agda/Compiler/JS/Compiler.hs b/src/full/Agda/Compiler/JS/Compiler.hs --- a/src/full/Agda/Compiler/JS/Compiler.hs +++ b/src/full/Agda/Compiler/JS/Compiler.hs @@ -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, diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs --- a/src/full/Agda/Interaction/BasicOps.hs +++ b/src/full/Agda/Interaction/BasicOps.hs @@ -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 diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs --- a/src/full/Agda/Syntax/Internal.hs +++ b/src/full/Agda/Syntax/Internal.hs @@ -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 - diff --git a/src/full/Agda/Syntax/Internal/Pattern.hs b/src/full/Agda/Syntax/Internal/Pattern.hs --- a/src/full/Agda/Syntax/Internal/Pattern.hs +++ b/src/full/Agda/Syntax/Internal/Pattern.hs @@ -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 diff --git a/src/full/Agda/Tests.hs b/src/full/Agda/Tests.hs --- a/src/full/Agda/Tests.hs +++ b/src/full/Agda/Tests.hs @@ -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 diff --git a/src/full/Agda/TypeChecking/Abstract.hs b/src/full/Agda/TypeChecking/Abstract.hs --- a/src/full/Agda/TypeChecking/Abstract.hs +++ b/src/full/Agda/TypeChecking/Abstract.hs @@ -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 diff --git a/src/full/Agda/TypeChecking/CheckInternal.hs b/src/full/Agda/TypeChecking/CheckInternal.hs --- a/src/full/Agda/TypeChecking/CheckInternal.hs +++ b/src/full/Agda/TypeChecking/CheckInternal.hs @@ -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') diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs --- a/src/full/Agda/TypeChecking/Coverage.hs +++ b/src/full/Agda/TypeChecking/Coverage.hs @@ -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 diff --git a/src/full/Agda/TypeChecking/Injectivity.hs b/src/full/Agda/TypeChecking/Injectivity.hs --- a/src/full/Agda/TypeChecking/Injectivity.hs +++ b/src/full/Agda/TypeChecking/Injectivity.hs @@ -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 $ diff --git a/src/full/Agda/TypeChecking/Polarity.hs b/src/full/Agda/TypeChecking/Polarity.hs --- a/src/full/Agda/TypeChecking/Polarity.hs +++ b/src/full/Agda/TypeChecking/Polarity.hs @@ -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. diff --git a/src/full/Agda/TypeChecking/Quote.hs b/src/full/Agda/TypeChecking/Quote.hs --- a/src/full/Agda/TypeChecking/Quote.hs +++ b/src/full/Agda/TypeChecking/Quote.hs @@ -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 - diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs --- a/src/full/Agda/TypeChecking/Reduce.hs +++ b/src/full/Agda/TypeChecking/Reduce.hs @@ -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 diff --git a/src/full/Agda/TypeChecking/Reduce/Monad.hs b/src/full/Agda/TypeChecking/Reduce/Monad.hs --- a/src/full/Agda/TypeChecking/Reduce/Monad.hs +++ b/src/full/Agda/TypeChecking/Reduce/Monad.hs @@ -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 diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs --- a/src/full/Agda/TypeChecking/Rules/Decl.hs +++ b/src/full/Agda/TypeChecking/Rules/Decl.hs @@ -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 ) diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs --- a/src/full/Agda/TypeChecking/Rules/Def.hs +++ b/src/full/Agda/TypeChecking/Rules/Def.hs @@ -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 ] diff --git a/src/full/Agda/TypeChecking/Rules/LHS.hs b/src/full/Agda/TypeChecking/Rules/LHS.hs --- a/src/full/Agda/TypeChecking/Rules/LHS.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS.hs @@ -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' diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs --- a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs @@ -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 $ diff --git a/src/full/Agda/TypeChecking/Rules/Record.hs b/src/full/Agda/TypeChecking/Rules/Record.hs --- a/src/full/Agda/TypeChecking/Rules/Record.hs +++ b/src/full/Agda/TypeChecking/Rules/Record.hs @@ -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 diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs --- a/src/full/Agda/TypeChecking/Rules/Term.hs +++ b/src/full/Agda/TypeChecking/Rules/Term.hs @@ -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) diff --git a/src/full/Agda/TypeChecking/Telescope.hs b/src/full/Agda/TypeChecking/Telescope.hs --- a/src/full/Agda/TypeChecking/Telescope.hs +++ b/src/full/Agda/TypeChecking/Telescope.hs @@ -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) diff --git a/src/full/Agda/TypeChecking/Unquote.hs b/src/full/Agda/TypeChecking/Unquote.hs new file mode 100644 --- /dev/null +++ b/src/full/Agda/TypeChecking/Unquote.hs @@ -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 diff --git a/src/full/Agda/Utils/FileName.hs b/src/full/Agda/Utils/FileName.hs --- a/src/full/Agda/Utils/FileName.hs +++ b/src/full/Agda/Utils/FileName.hs @@ -76,7 +76,7 @@ | otherwise = __IMPOSSIBLE__ #if mingw32_HOST_OS -prop_mkAbsolute :: FilePath -> Propertty +prop_mkAbsolute :: FilePath -> Property #else prop_mkAbsolute :: FilePath -> Bool #endif diff --git a/src/full/Agda/Utils/Permutation.hs b/src/full/Agda/Utils/Permutation.hs --- a/src/full/Agda/Utils/Permutation.hs +++ b/src/full/Agda/Utils/Permutation.hs @@ -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' +------------------------------------------------------------------------ diff --git a/src/full/Agda/Utils/Permutation/Tests.hs b/src/full/Agda/Utils/Permutation/Tests.hs new file mode 100644 --- /dev/null +++ b/src/full/Agda/Utils/Permutation/Tests.hs @@ -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 diff --git a/src/full/Agda/Utils/VarSet.hs b/src/full/Agda/Utils/VarSet.hs --- a/src/full/Agda/Utils/VarSet.hs +++ b/src/full/Agda/Utils/VarSet.hs @@ -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