module Agda.TypeChecking.CompiledClause.Compile where
import Prelude hiding (null)
import Control.Monad
import Data.Maybe
import Data.Monoid
import qualified Data.Map as Map
import Data.List (nubBy)
import Data.Function
import Debug.Trace
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Monad
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty (prettyTCM, nest, sep, text)
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.List
import Agda.Utils.Pretty (Pretty(..), prettyShow)
import qualified Agda.Utils.Pretty as P
#include "undefined.h"
import Agda.Utils.Impossible
compileClauses ::
Maybe (QName, Type)
-> [Clause] -> TCM CompiledClauses
compileClauses mt cs = do
cs <- normaliseProjP cs
let unBruijn cs = [ Cl (map (fmap (fmap dbPatVarName . namedThing)) $ namedClausePats c)
(compiledClauseBody c) | c <- cs ]
shared <- sharedFun
case mt of
Nothing -> return $ compile shared $ unBruijn cs
Just (q, t) -> do
splitTree <- coverageCheck q t cs
cs <- normaliseProjP =<< defClauses <$> getConstInfo q
let cls = unBruijn cs
reportSDoc "tc.cc" 30 $ sep $ do
(text "clauses patterns before compilation") : do
map (prettyTCM . map unArg . clPats) cls
reportSDoc "tc.cc" 50 $ do
sep [ text "clauses before compilation"
, (nest 2 . text . show) cs
]
let cc = compileWithSplitTree shared splitTree cls
reportSDoc "tc.cc" 12 $ sep
[ text "compiled clauses (still containing record splits)"
, nest 2 $ return $ P.pretty cc
]
cc <- translateCompiledClauses cc
return cc
data Cl = Cl
{ clPats :: [Arg Pattern]
, clBody :: Maybe Term
} deriving (Show)
instance Pretty Cl where
pretty (Cl ps b) = P.prettyList ps P.<+> P.text "->" P.<+> maybe (P.text "_|_") pretty b
type Cls = [Cl]
compileWithSplitTree :: (Term -> Term) -> SplitTree -> Cls -> CompiledClauses
compileWithSplitTree shared t cs = case t of
SplitAt i ts -> Case i $ compiles ts $ splitOn (length ts == 1) (unArg i) cs
SplittingDone n -> compile shared cs
where
compiles :: SplitTrees -> Case Cls -> Case CompiledClauses
compiles ts br@Branches{ projPatterns = cop
, conBranches = cons
, litBranches = lits
, catchAllBranch = catchAll }
= Branches
{ projPatterns = cop
, conBranches = updCons cons
, litBranches = compile shared <$> lits
, catchAllBranch = compile shared <$> catchAll
}
where
updCons = Map.mapWithKey $ \ c cl ->
caseMaybe (lookup c ts) (compile shared) (compileWithSplitTree shared) <$> cl
compile :: (Term -> Term) -> Cls -> CompiledClauses
compile shared cs = case nextSplit cs of
Just (isRecP, n)-> Case n $ fmap (compile shared) $ splitOn isRecP (unArg n) cs
Nothing -> case clBody c of
Just t -> Done (map (fmap name) $ clPats c) (shared t)
Nothing -> Fail
where
c = headWithDefault __IMPOSSIBLE__ cs
name (VarP x) = x
name (DotP _) = underscore
name AbsurdP{} = absurdPatternName
name ConP{} = __IMPOSSIBLE__
name LitP{} = __IMPOSSIBLE__
name ProjP{} = __IMPOSSIBLE__
nextSplit :: Cls -> Maybe (Bool, Arg Int)
nextSplit [] = __IMPOSSIBLE__
nextSplit (Cl ps _ : _) = headMaybe $ catMaybes $
zipWith (\ (Arg ai p) n -> (, Arg ai n) <$> properSplit p) ps [0..]
properSplit :: Pattern' a -> Maybe Bool
properSplit (ConP _ cpi _) = Just $ isJust $ conPRecord cpi
properSplit LitP{} = Just False
properSplit ProjP{} = Just False
properSplit VarP{} = Nothing
properSplit AbsurdP{} = Nothing
properSplit DotP{} = Nothing
isVar :: Pattern' a -> Bool
isVar VarP{} = True
isVar DotP{} = True
isVar AbsurdP{} = True
isVar ConP{} = False
isVar LitP{} = False
isVar ProjP{} = False
splitOn :: Bool -> Int -> Cls -> Case Cls
splitOn single n cs = mconcat $ map (fmap (:[]) . splitC n) $
expandCatchAlls single n cs
splitC :: Int -> Cl -> Case Cl
splitC n (Cl ps b) = caseMaybe mp fallback $ \case
ProjP _ d -> projCase d $ Cl (ps0 ++ ps1) b
ConP c _ qs -> conCase (conName c) $ WithArity (length qs) $
Cl (ps0 ++ map (fmap namedThing) qs ++ ps1) b
LitP l -> litCase l $ Cl (ps0 ++ ps1) b
VarP{} -> fallback
DotP{} -> fallback
AbsurdP{} -> fallback
where
(ps0, rest) = splitAt n ps
mp = unArg <$> headMaybe rest
ps1 = drop 1 rest
fallback = catchAll $ Cl ps b
expandCatchAlls :: Bool -> Int -> Cls -> Cls
expandCatchAlls single n cs =
if single then doExpand =<< cs else
case cs of
_ | all (isCatchAllNth . clPats) cs -> cs
c@(Cl ps b) : cs | not (isCatchAllNth ps) -> c : expandCatchAlls False n cs
| otherwise -> map (expand c) expansions ++ c : expandCatchAlls False n cs
_ -> __IMPOSSIBLE__
where
doExpand c@(Cl ps _)
| exCatchAllNth ps = map (expand c) expansions ++ [c]
| otherwise = [c]
isCatchAllNth ps = all (isVar . unArg) $ take 1 $ drop n ps
exCatchAllNth ps = any (isVar . unArg) $ take 1 $ drop n ps
classify (LitP l) = Left l
classify (ConP c _ _) = Right c
classify _ = __IMPOSSIBLE__
expansions = nubBy ((==) `on` (classify . unArg . snd))
. mapMaybe (notVarNth . clPats)
$ cs
notVarNth
:: [Arg Pattern]
-> Maybe ([Arg Pattern]
, Arg Pattern)
notVarNth ps = do
let (ps1, ps2) = splitAt n ps
p <- headMaybe ps2
guard $ not $ isVar $ unArg p
return (ps1, p)
expand cl (qs, q) =
case unArg q of
ConP c mt qs' -> Cl (ps0 ++ [q $> ConP c mt conPArgs] ++ ps1)
(substBody n' m (Con c ci conArgs) b)
where
ci = fromConPatternInfo mt
m = length qs'
conPArgs = map (fmap ($> VarP "_")) qs'
conArgs = zipWith (\ q' i -> q' $> var i) qs' $ downFrom m
LitP l -> Cl (ps0 ++ [q $> LitP l] ++ ps1) (substBody n' 0 (Lit l) b)
_ -> __IMPOSSIBLE__
where
Cl ps b = ensureNPatterns (n + 1) (map getArgInfo $ qs ++ [q]) cl
(ps0, _:ps1) = splitAt n ps
n' = countVars ps1
countVars = sum . map (count . unArg)
count VarP{} = 1
count (ConP _ _ ps) = countVars $ map (fmap namedThing) ps
count DotP{} = 1
count (AbsurdP p) = count p
count _ = 0
ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
ensureNPatterns n ais0 cl@(Cl ps b)
| m <= 0 = cl
| otherwise = Cl (ps ++ ps') (raise m b `apply` args)
where
k = length ps
ais = drop k ais0
m = n k
ps' = for ais $ \ ai -> Arg ai $ VarP "_"
args = zipWith (\ i ai -> Arg ai $ var i) (downFrom m) ais
substBody :: (Subst t a) => Int -> Int -> t -> a -> a
substBody n m v = applySubst $ liftS n $ v :# raiseS m