module Agda.TypeChecking.RecordPatterns
( translateRecordPatterns
) where
import Control.Applicative
import Control.Arrow ((***))
import Control.Monad.Fix
import Control.Monad.Reader
import Control.Monad.State
import Data.List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute hiding (Subst)
import Agda.TypeChecking.Telescope
import Agda.Utils.Either
import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "../undefined.h"
import Agda.Utils.Impossible
translateRecordPatterns :: MonadTCM tcm => Clause -> tcm Clauses
translateRecordPatterns clause = do
(ps, s, cs) <- runRecPatM $ translatePatterns $ clausePats clause
let
noNewPatternVars = size cs
rhsSubst = map (\t -> t rhsSubst') (reverse s) ++
[ Var i [] | i <- [noNewPatternVars..] ]
rhsSubst' = permute (reverseP $ clausePerm clause) init ++ rest
where (init, rest) = genericSplitAt (size s) rhsSubst
flattenedOldTel =
permute (invertP $ compactP $ clausePerm clause) $
zip (teleNames $ clauseTel clause) $
flattenTel $
clauseTel clause
newTel' =
map (fmap (id *** substs rhsSubst')) $
translateTel cs $
flattenedOldTel
newPerm = adjustForDotPatterns $
reorderTel $ map (maybe dummy snd) newTel'
where
dummy = defaultArg (El Prop (Sort Prop))
isDotP n = case genericIndex cs n of
Left DotP{} -> True
_ -> False
adjustForDotPatterns (Perm n is) =
Perm n (filter (not . isDotP) is)
lhsSubst' = permToSubst (reverseP newPerm)
lhsSubst = map (substs lhsSubst') rhsSubst'
newTel =
uncurry unflattenTel . unzip $
map (maybe __IMPOSSIBLE__ id) $
permute newPerm $
map (fmap (id *** substs lhsSubst')) $
newTel'
c = clause
{ clauseTel = newTel
, clausePerm = newPerm
, clausePats = substs lhsSubst ps
, clauseBody = translateBody cs rhsSubst $ clauseBody clause
}
reportSDoc "tc.lhs.top" 10 $
escapeContext (size $ clauseTel clause) $ vcat
[ text "Translated clause:"
, nest 2 $ vcat
[ text "delta =" <+> prettyTCM (clauseTel c)
, text "perm =" <+> text (show $ clausePerm c)
, text "ps =" <+> text (show $ clausePats c)
, text "body =" <+> text (show $ clauseBody c)
, text "body =" <+> prettyTCM (clauseBody c)
]
]
return $ Clauses { translatedClause = c
, maybeOriginalClause =
if all isLeft cs then Nothing else Just clause
}
newtype RecPatM a = RecPatM (TCMT (ReaderT Nat (StateT Nat IO)) a)
deriving (Functor, Applicative, Monad,
MonadIO, MonadTCM,
MonadReader TCEnv, MonadState TCState)
runRecPatM :: MonadTCM tcm => RecPatM a -> tcm a
runRecPatM (RecPatM m) = liftTCM $
mapTCMT (\m -> do
(x, noVars) <- mfix $ \ ~(_, noVars) ->
runStateT (runReaderT m noVars) 0
return x)
m
nextVar :: RecPatM (Pattern, Term)
nextVar = RecPatM $ do
n <- lift get
lift $ put $ succ n
noVars <- lift ask
return (VarP "r", Var (noVars n 1) [])
data Kind = VarPat | DotPat
deriving Eq
type Subst = [Substitution -> Term]
type Changes = [Either Pattern (Kind -> Nat, String, Arg Type)]
data RecordTree
= Leaf Pattern
| RecCon (Arg Type) [(Substitution -> Term -> Term, RecordTree)]
projections :: RecordTree -> [(Substitution -> Term -> Term, Kind)]
projections (Leaf (DotP{})) = [(flip const, DotPat)]
projections (Leaf (VarP{})) = [(flip const, VarPat)]
projections (Leaf _) = __IMPOSSIBLE__
projections (RecCon _ args) =
concatMap (\(p, t) -> map (\(t, k) -> (\s -> t s . p s, k))
(projections t))
args
removeTree :: RecordTree -> RecPatM (Pattern, Subst, Changes)
removeTree tree = do
(pat, x) <- nextVar
let ps = projections tree
s = map (\(p, _) -> \s -> p s x) ps
count k = genericLength $ filter ((== k) . snd) ps
dotPatternInside = case tree of
Leaf {} -> False
RecCon {} -> any ((== DotPat) . snd) ps
if dotPatternInside then
typeError $ NotSupported $
"Dot patterns inside record patterns, " ++
"unless accompanied by data type patterns"
else
return $ case tree of
Leaf p -> (p, s, [Left p])
RecCon t _ -> (pat, s, [Right (count, "r", t)])
translatePattern :: Pattern -> RecPatM (Pattern, Subst, Changes)
translatePattern (ConP c Nothing ps) = do
(ps, s, cs) <- translatePatterns ps
return (ConP c Nothing ps, s, cs)
translatePattern p@(ConP _ (Just _) _) = do
r <- recordTree p
case r of
Left r -> r
Right t -> removeTree t
translatePattern p@VarP{} = removeTree (Leaf p)
translatePattern p@DotP{} = removeTree (Leaf p)
translatePattern p@LitP{} = return (p, [], [])
translatePatterns ::
[Arg Pattern] -> RecPatM ([Arg Pattern], Subst, Changes)
translatePatterns ps = do
(ps', ss, cs) <- unzip3 <$> mapM (translatePattern . unArg) ps
return (ps' `withArgsFrom` ps, concat ss, concat cs)
recordTree ::
Pattern ->
RecPatM (Either (RecPatM (Pattern, Subst, Changes)) RecordTree)
recordTree p@(ConP _ Nothing _) = return $ Left $ translatePattern p
recordTree (ConP c (Just t) ps) = do
rs <- mapM (recordTree . unArg) ps
case allRight rs of
Left rs ->
return $ Left $ do
(ps', ss, cs) <- unzip3 <$> mapM (either id removeTree) rs
return (ConP c (Just t) (ps' `withArgsFrom` ps),
concat ss, concat cs)
Right ts -> do
t <- reduce t
case t of
Arg { unArg = El _ (Def r args) } -> do
rDef <- theDef <$> getConstInfo r
case rDef of
Record { recFields = fields } -> do
let proj p = \s t ->
Def (unArg p) (substs s (map hide args) ++ [defaultArg t])
return $ Right $ RecCon t $ zip (map proj fields) ts
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
recordTree p@VarP{} = return (Right (Leaf p))
recordTree p@DotP{} = return (Right (Leaf p))
recordTree p@LitP{} = return $ Left $ translatePattern p
translateTel
:: Changes
-> [(String, Arg Type)]
-> [Maybe (String, Arg Type)]
translateTel (Left (DotP{}) : rest) tel = Nothing : translateTel rest tel
translateTel (Right (n, x, t) : rest) tel = Just (x, t) :
translateTel rest
(genericDrop (n VarPat) tel)
translateTel (Left _ : rest) (t : tel) = Just t : translateTel rest tel
translateTel [] [] = []
translateTel (Left _ : _) [] = __IMPOSSIBLE__
translateTel [] (_ : _) = __IMPOSSIBLE__
translateBody :: Changes -> Substitution -> ClauseBody -> ClauseBody
translateBody _ s NoBody = NoBody
translateBody (Right (n, x, _) : rest) s b =
Bind $ Abs x $ translateBody rest s $ dropBinds n' b
where n' = sum $ map n [VarPat, DotPat]
translateBody (Left _ : rest) s (Bind b) = Bind $ fmap (translateBody rest s) b
translateBody (Left _ : rest) s (NoBind b) = NoBind $ translateBody rest s b
translateBody [] s (Body t) = Body $ substs s t
translateBody _ _ _ = __IMPOSSIBLE__
permToSubst :: Permutation -> Substitution
permToSubst (Perm n is) =
[ makeVar i | i <- [0..n1] ] ++ [ Var i [] | i <- [size is..] ]
where
makeVar i = case genericElemIndex i is of
Nothing -> __IMPOSSIBLE__
Just k -> Var k []
dropBinds :: Nat -> ClauseBody -> ClauseBody
dropBinds n b | n == 0 = b
dropBinds n (Bind b) | n > 0 = dropBinds (pred n) (absBody b)
dropBinds n (NoBind b) | n > 0 = dropBinds (pred n) b
dropBinds _ _ = __IMPOSSIBLE__