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, piApply, 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
import Agda.Utils.Lens
dataParameters :: QName -> Compile TCM Nat
dataParameters = lift . dataParametersTCM
dataParametersTCM :: QName -> TCM Nat
dataParametersTCM name = do
m <- use $ stImports . sigDefinitions
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 :: Int -> TCM P.Doc -> Compile TCM ()
report n s = 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.ignoreSharing . 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 0 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 :: QName -> Int -> Term
mkCon c n = I.Con (I.ConHead c Inductive []) $ map (defaultArg . I.var) $ downFrom n
unifyI :: Telescope -> FlexibleVars -> Type -> Args -> Args -> Compile TCM [Maybe Term]
unifyI tele flex typ a1 a2 = lift $ typeError $ NotImplemented "using the new unification algorithm for forcing"
takeTele :: Int -> Telescope -> Telescope
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 $ use $ stImports . sigDefinitions
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 (I.ignoreSharing $ unEl ntyp, I.ignoreSharing $ 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 `piApply` 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.Shared p) = buildTerm var idx $ I.derefPtr p
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 I.ignoreSharing 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