module Agda.Compiler.Epic.Forcing where
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Data.Char
import Data.List hiding (sort)
import Data.Maybe
import Agda.Syntax.Common
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position(noRange)
import Agda.Syntax.Internal(Tele(..), Telescope, Term, Abs(..), unAbs, absName, Type, Args, QName, unEl)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Rules.LHS.Problem (FlexibleVars, defaultFlexibleVar)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Substitute
(applySubst, apply, wkS, raiseS, dropS, (++#), TelV(..))
import qualified Agda.TypeChecking.Substitute as S
import Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Size
import qualified Agda.Utils.HashMap as HM
import Agda.Compiler.Epic.AuxAST
import Agda.Compiler.Epic.CompileState
import Agda.Compiler.Epic.Epic
import Agda.Compiler.Epic.Interface
import qualified Agda.Compiler.Epic.FromAgda as FA
#include "../../undefined.h"
import Agda.Utils.Impossible
dataParameters :: QName -> Compile TCM Nat
dataParameters = lift . dataParametersTCM
dataParametersTCM :: QName -> TCM Nat
dataParametersTCM name = do
m <- (gets (sigDefinitions . stImports))
return $ maybe __IMPOSSIBLE__ (defnPars . theDef) (HM.lookup name m)
where
defnPars :: Defn -> Nat
defnPars (Datatype {dataPars = p}) = p
defnPars (Record {recPars = p}) = p
defnPars d = 0
report n s = do
lift $ reportSDoc "epic.forcing" n s
piApplyM' :: Type -> Args -> TCM Type
piApplyM' t as = do
piApplyM t as
insertTele ::(QName, Args) -> Int
-> Maybe Type
-> Term
-> Telescope
-> Compile TCM ( Telescope
, ( Telescope
, Type
, Type
)
)
insertTele x 0 ins term (ExtendTel t to) = do
t' <- lift $ normalise t
report 12 $ vcat
[ text "t' :" <+> prettyTCM t'
, text "term:" <+> prettyTCM term
, text "to:" <+> prettyTCM (unAbs to)
]
(st, arg) <- case I.unEl . unDom $ t' of
I.Def st es -> return (st, fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es)
s -> do
report 10 $ vcat
[ text "ERROR!!!"
, text "found: " <+> (text . show) s
, text "ins" <+> (prettyTCM . fromMaybe __IMPOSSIBLE__) ins
]
return x
pars <- dataParameters st
report 10 $ text "apply in insertTele"
TelV ctele ctyp <- lift $ telView =<< maybe (return $ unDom t')
(`piApplyM'` genericTake pars arg) ins
when (genericLength arg < pars) __IMPOSSIBLE__
return ( ctele +:+ (S.subst term $ S.raiseFrom 1 (size ctele) (unAbs to))
, (ctele, S.raise (size ctele) $ unDom t , ctyp)
)
where
(+:+) :: Telescope -> Telescope -> Telescope
EmptyTel +:+ t2 = t2
ExtendTel t t1 +:+ t2 = ExtendTel t (Abs (absName t1) $ unAbs t1 +:+ t2 )
insertTele x n ins term EmptyTel = __IMPOSSIBLE__
insertTele er n ins term (ExtendTel x xs) = do
(xs', typ) <- insertTele er (n 1) ins term (unAbs xs)
return (ExtendTel x $ Abs (absName xs) xs' , typ)
mkCon c n = I.Con (I.ConHead c []) [ defaultArg $ I.Var (fromIntegral i) [] | i <- [n 1, n 2 .. 0] ]
unifyI :: Telescope -> FlexibleVars -> Type -> Args -> Args -> Compile TCM [Maybe Term]
unifyI tele flex typ a1 a2 = lift $ addCtxTel tele $ unifyIndices_ flex typ a1 a2
takeTele 0 _ = EmptyTel
takeTele n (ExtendTel t ts) = ExtendTel t $ Abs (absName ts) $ takeTele (n1) (unAbs ts)
takeTele _ _ = __IMPOSSIBLE__
remForced :: [Fun] -> Compile TCM [Fun]
remForced fs = do
defs <- lift (gets (sigDefinitions . stImports))
forM fs $ \f -> case f of
Fun{} -> case funQName f >>= flip HM.lookup defs of
Nothing -> __IMPOSSIBLE__
Just def -> do
TelV tele _ <- lift $ telView (defType def)
report 10 $ vcat
[ text "compiling fun" <+> (text . show) (funQName f)
]
e <- forcedExpr (funArgs f) tele (funExpr f)
report 10 $ vcat
[ text "compilied fun" <+> (text . show) (funQName f)
, text "before:" <+> (text . prettyEpic) (funExpr f)
, text "after:" <+> (text . prettyEpic) e
]
return $ f { funExpr = e}
EpicFun{} -> return f
forcedExpr :: [Var] -> Telescope -> Expr -> Compile TCM Expr
forcedExpr vars tele expr = case expr of
Var _ -> return expr
Lit _ -> return expr
Lam x e -> Lam x <$> rec e
Con t q es -> Con t q <$> mapM rec es
App v es -> App v <$> mapM rec es
If a b c -> If <$> rec a <*> rec b <*> rec c
Let v e1 e2 -> Let v <$> rec e1 <*> rec e2
Lazy e -> Lazy <$> rec e
UNIT -> return expr
IMPOSSIBLE -> return expr
Case v@(Var x) brs -> do
let n = fromMaybe __IMPOSSIBLE__ $ elemIndex x vars
(Case v <$>) . forM brs $ \ br -> case br of
BrInt i e -> do
(tele'', _) <- insertTele __IMPOSSIBLE__ n Nothing (I.Lit (LitChar noRange (chr i))) tele
BrInt i <$> forcedExpr (replaceAt n vars []) tele'' e
Default e -> Default <$> rec e
Branch t constr as e -> do
typ <- getType constr
forc <- getForcedArgs constr
(tele'', (_, ntyp, ctyp)) <- insertTele __IMPOSSIBLE__ n (Just typ)
(mkCon constr (length as)) tele
ntyp <- lift $ reduce ntyp
ctyp <- lift $ reduce ctyp
if null (forced forc as)
then Branch t constr as <$> forcedExpr (replaceAt n vars as) tele'' e
else do
unif <- case (unEl ntyp, unEl ctyp) of
(I.Def st es1, I.Def st' es2) | st == st' -> do
let a1 = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es1
let a2 = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es2
typPars <- dataParameters st
setType <- getType st
report 10 $ vcat
[ text "ntyp:" <+> prettyTCM ntyp
, text "ctyp:" <+> prettyTCM ctyp
]
unifyI (takeTele (n + length as) tele'')
(map defaultFlexibleVar [0 .. n + length as])
(setType `apply` take typPars a1)
(drop typPars a1)
(drop typPars a2)
_ -> __IMPOSSIBLE__
let
lower = wkS (1) . dropS 1
subT 0 tel = let ss = [fromMaybe (I.Var n []) t
| (n , t) <- zip [0..] unif] ++#
raiseS (length unif)
in (applySubst ss tel, lower ss)
subT n (ExtendTel a t) = let
(tb' , ss) = subT (n 1) (unAbs t)
in (ExtendTel a $ Abs (absName t) tb', lower ss)
subT _ _ = __IMPOSSIBLE__
(tele'''', _) = subT (n + length as) tele''
report 10 $ nest 2 $ vcat
[ text "remforced"
, text "tele=" <+> prettyTCM tele''
, text "tele'=" <+> prettyTCM tele''''
, text "unif=" <+> (text . show) unif
, text "forced=" <+> (text . show) (forced forc as)
, text "constr" <+> prettyTCM constr
]
Branch t constr as <$>
replaceForced (replaceAt n vars as, reverse $ take n vars ++ as)
(tele'''') (forced forc as) unif e
_ -> __IMPOSSIBLE__
where
rec = forcedExpr vars tele
replaceForced :: ([Var],[Var]) -> Telescope -> [Var] -> [Maybe I.Term] -> Expr -> Compile TCM Expr
replaceForced (vars,_) tele [] _ e = forcedExpr vars tele e
replaceForced (vars,uvars) tele (fvar : fvars) unif e = do
let n = fromMaybe __IMPOSSIBLE__ $ elemIndex fvar uvars
mpos <- findPosition n unif
case mpos of
Nothing -> case fromMaybe __IMPOSSIBLE__ $ unif !!! n of
Nothing | fvar `notElem` fv e ->
replaceForced (vars, uvars) tele fvars unif e
Nothing -> do
report 10 $ vcat
[ text "failure comming!"
, text "unif" <+> (text . show) unif
, text "n" <+> (text . show) n
, text "fvar" <+> (text fvar)
, text "fv" <+> (text . show) (fv e)
]
__IMPOSSIBLE__
Just t -> do
v <- newName
te <- FA.substTerm uvars t
subst fvar v <$> replaceForced (vars, uvars)
tele fvars unif (Let v te e)
Just (pos , term) -> do
(build, v) <- buildTerm (fromMaybe __IMPOSSIBLE__ $ uvars !!! pos) n term
build . subst fvar v <$> replaceForced (vars, uvars) tele fvars unif
e
where
sub fvar v = map $ \x -> if x == fvar then v else x
buildTerm :: Var -> Nat -> Term -> Compile TCM (Expr -> Expr, Var)
buildTerm var idx (I.Var i _) | idx == i = return (id, var)
buildTerm var idx (I.Con con args) = do
let c = I.conName con
vs <- replicateM (length args) newName
(pos , arg) <- fromMaybe __IMPOSSIBLE__ <$> findPosition idx (map (Just . unArg) args)
(fun2 , v) <- buildTerm (fromMaybe __IMPOSSIBLE__ $ vs !!! pos) idx arg
tag <- getConstrTag c
let fun1 e = casee (Var var) [Branch tag c vs e]
return (fun1 . fun2 , v)
buildTerm _ _ _ = __IMPOSSIBLE__
findPosition :: Nat -> [Maybe I.Term] -> Compile TCM (Maybe (Nat, I.Term))
findPosition var ts = (listToMaybe . catMaybes <$>) . forM (zip [0..] ts) $ \ (n, mt) -> do
ifM (maybe (return False) pred mt)
(return (Just (n, fromMaybe __IMPOSSIBLE__ mt)))
(return Nothing)
where
pred :: Term -> Compile TCM Bool
pred t = case t of
I.Var i _ | var == i -> return True
I.Con c args -> do
forc <- getForcedArgs $ I.conName c
or <$> mapM (pred . unArg) (notForced forc args)
_ -> return False