module Agda.TypeChecking.Reduce where
import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Applicative
import Data.List as List hiding (sort)
import Data.Maybe
import Data.Map (Map)
import Data.Traversable
import Data.Hashable
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Base (Scope)
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad hiding ( underAbstraction_, enterClosure, isInstantiatedMeta
, reportSDoc, reportSLn, getConstInfo
, lookupMeta )
import qualified Agda.TypeChecking.Monad as TCM
import Agda.TypeChecking.Monad.Builtin hiding (getPrimitive, constructorForm)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Patterns.Match
import Agda.TypeChecking.CompiledClause.Match
import Agda.TypeChecking.Reduce.Monad
import Agda.Utils.Monad
import Agda.Utils.HashMap (HashMap)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
instantiate :: Instantiate a => a -> TCM a
instantiate = runReduceM . instantiate'
instantiateFull :: InstantiateFull a => a -> TCM a
instantiateFull = runReduceM . instantiateFull'
reduce :: Reduce a => a -> TCM a
reduce = runReduceM . reduce'
reduceB :: Reduce a => a -> TCM (Blocked a)
reduceB = runReduceM . reduceB'
normalise :: Normalise a => a -> TCM a
normalise = runReduceM . normalise'
simplify :: Simplify a => a -> TCM a
simplify = runReduceM . simplify'
class Instantiate t where
instantiate' :: t -> ReduceM t
instance Instantiate Term where
instantiate' t@(MetaV x es) = do
mi <- mvInstantiation <$> lookupMeta x
case mi of
InstV tel v -> instantiate' inst
where
(es1, es2) = splitAt (length tel) es
vs1 = reverse $ map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es1
rho = vs1 ++# wkS (length vs1) idS
inst = applySubst rho (foldr mkLam v $ drop (length es1) tel) `applyE` es2
Open -> return t
OpenIFS -> return t
BlockedConst _ -> return t
PostponedTypeCheckingProblem _ _ -> return t
InstS _ -> __IMPOSSIBLE__
instantiate' (Level l) = levelTm <$> instantiate' l
instantiate' (Sort s) = sortTm <$> instantiate' s
instantiate' v@Shared{} =
__IMPOSSIBLE__
instantiate' t = return t
instance Instantiate Level where
instantiate' (Max as) = levelMax <$> instantiate' as
instance Instantiate PlusLevel where
instantiate' l@ClosedLevel{} = return l
instantiate' (Plus n a) = Plus n <$> instantiate' a
instance Instantiate LevelAtom where
instantiate' l = case l of
MetaLevel m vs -> do
v <- instantiate' (MetaV m vs)
case ignoreSharing v of
MetaV m vs -> return $ MetaLevel m vs
_ -> return $ UnreducedLevel v
UnreducedLevel l -> UnreducedLevel <$> instantiate' l
_ -> return l
instance Instantiate a => Instantiate (Blocked a) where
instantiate' v@NotBlocked{} = return v
instantiate' v@(Blocked x u) = do
mi <- mvInstantiation <$> lookupMeta x
case mi of
InstV{} -> notBlocked <$> instantiate' u
Open -> return v
OpenIFS -> return v
BlockedConst{} -> return v
PostponedTypeCheckingProblem{} -> return v
InstS{} -> __IMPOSSIBLE__
instance Instantiate Type where
instantiate' (El s t) = El <$> instantiate' s <*> instantiate' t
instance Instantiate Sort where
instantiate' s = case s of
Type l -> levelSort <$> instantiate' l
_ -> return s
instance Instantiate Elim where
instantiate' (Apply v) = Apply <$> instantiate' v
instantiate' (Proj f) = pure $ Proj f
instance Instantiate t => Instantiate (Abs t) where
instantiate' = traverse instantiate'
instance Instantiate t => Instantiate (Arg t) where
instantiate' = traverse instantiate'
instance Instantiate t => Instantiate (Dom t) where
instantiate' = traverse instantiate'
instance Instantiate t => Instantiate [t] where
instantiate' = traverse instantiate'
instance (Instantiate a, Instantiate b) => Instantiate (a,b) where
instantiate' (x,y) = (,) <$> instantiate' x <*> instantiate' y
instance (Instantiate a, Instantiate b,Instantiate c) => Instantiate (a,b,c) where
instantiate' (x,y,z) = (,,) <$> instantiate' x <*> instantiate' y <*> instantiate' z
instance Instantiate a => Instantiate (Closure a) where
instantiate' cl = do
x <- enterClosure cl instantiate'
return $ cl { clValue = x }
instance Instantiate Telescope where
instantiate' tel = return tel
instance Instantiate Constraint where
instantiate' (ValueCmp cmp t u v) = do
(t,u,v) <- instantiate' (t,u,v)
return $ ValueCmp cmp t u v
instantiate' (ElimCmp cmp t v as bs) =
ElimCmp cmp <$> instantiate' t <*> instantiate' v <*> instantiate' as <*> instantiate' bs
instantiate' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> instantiate' (u,v)
instantiate' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> instantiate' (a,b)
instantiate' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> instantiate' (tela,telb)
instantiate' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> instantiate' (a,b)
instantiate' (Guarded c pid) = Guarded <$> instantiate' c <*> pure pid
instantiate' (UnBlock m) = return $ UnBlock m
instantiate' (FindInScope m args) = FindInScope m <$> mapM instantiate' args
instantiate' (IsEmpty r t) = IsEmpty r <$> instantiate' t
instance (Ord k, Instantiate e) => Instantiate (Map k e) where
instantiate' = traverse instantiate'
ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (Term -> tcm a) -> tcm a
ifBlocked t blocked unblocked = do
t <- liftTCM $ reduceB t
case ignoreSharing <$> t of
Blocked m _ -> blocked m (ignoreBlocking t)
NotBlocked (MetaV m _) -> blocked m (ignoreBlocking t)
NotBlocked _ -> unblocked (ignoreBlocking t)
ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm a
ifBlockedType (El s t) blocked unblocked =
ifBlocked t (\ m v -> blocked m $ El s v) (\ v -> unblocked $ El s v)
class Reduce t where
reduce' :: t -> ReduceM t
reduceB' :: t -> ReduceM (Blocked t)
reduce' t = ignoreBlocking <$> reduceB' t
reduceB' t = notBlocked <$> reduce' t
instance Reduce Type where
reduce' (El s t) = El s <$> reduce' t
reduceB' (El s t) = fmap (El s) <$> reduceB' t
instance Reduce Sort where
reduce' s =
ifNotM hasUniversePolymorphism (red s) $ red =<< instantiateFull' s
where
red s = do
s <- instantiate' s
case s of
DLub s1 s2 -> do
s <- dLub <$> reduce' s1 <*> reduce' s2
case s of
DLub{} -> return s
_ -> reduce' s
Prop -> return s
Type s' -> levelSort <$> reduce' s'
Inf -> return Inf
instance Reduce Elim where
reduce' (Apply v) = Apply <$> reduce' v
reduce' (Proj f) = pure $ Proj f
instance Reduce Level where
reduce' (Max as) = levelMax <$> mapM reduce' as
reduceB' (Max as) = fmap levelMax . traverse id <$> traverse reduceB' as
instance Reduce PlusLevel where
reduceB' l@ClosedLevel{} = return $ notBlocked l
reduceB' (Plus n l) = fmap (Plus n) <$> reduceB' l
instance Reduce LevelAtom where
reduceB' l = case l of
MetaLevel m vs -> fromTm (MetaV m vs)
NeutralLevel v -> return $ NotBlocked $ NeutralLevel v
BlockedLevel m v ->
ifM (isInstantiatedMeta m) (fromTm v) (return $ Blocked m $ BlockedLevel m v)
UnreducedLevel v -> fromTm v
where
fromTm v = do
bv <- reduceB' v
let v = ignoreBlocking bv
case ignoreSharing <$> bv of
NotBlocked (MetaV m vs) -> return $ NotBlocked $ MetaLevel m vs
Blocked m _ -> return $ Blocked m $ BlockedLevel m v
NotBlocked _ -> return $ NotBlocked $ NeutralLevel v
instance (Subst t, Reduce t) => Reduce (Abs t) where
reduce' b@(Abs x _) = Abs x <$> underAbstraction_ b reduce'
reduce' (NoAbs x v) = NoAbs x <$> reduce' v
instance Reduce t => Reduce [t] where
reduce' = traverse reduce'
instance Reduce t => Reduce (Arg t) where
reduce' a = case getRelevance a of
Irrelevant -> return a
_ -> traverse reduce' a
reduceB' t = traverse id <$> traverse reduceB' t
instance Reduce t => Reduce (Dom t) where
reduce' = traverse reduce'
reduceB' t = traverse id <$> traverse reduceB' t
instance (Reduce a, Reduce b) => Reduce (a,b) where
reduce' (x,y) = (,) <$> reduce' x <*> reduce' y
instance (Reduce a, Reduce b,Reduce c) => Reduce (a,b,c) where
reduce' (x,y,z) = (,,) <$> reduce' x <*> reduce' y <*> reduce' z
instance Reduce Term where
reduceB' v = do
v <- instantiate' v
let done = return $ notBlocked v
case v of
MetaV x es -> done
Def f es -> unfoldDefinitionE False reduceB' (Def f []) f es
Con c args -> do
v <- unfoldDefinition False reduceB' (Con c []) (conName c) args
traverse reduceNat v
Sort s -> fmap sortTm <$> reduceB' s
Level l -> ifM (elem LevelReductions <$> asks envAllowedReductions)
(fmap levelTm <$> reduceB' l)
done
Pi _ _ -> done
Lit _ -> done
Var _ _ -> done
Lam _ _ -> done
DontCare _ -> done
ExtLam{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
where
reduceNat v@Shared{} = __IMPOSSIBLE__
reduceNat v@(Con c []) = do
mz <- getBuiltin' builtinZero
case v of
_ | Just v == mz -> return $ Lit $ LitInt (getRange c) 0
_ -> return v
reduceNat v@(Con c [a]) | notHidden a && isRelevant a = do
ms <- fmap ignoreSharing <$> getBuiltin' builtinSuc
case v of
_ | Just (Con c []) == ms -> inc <$> reduce' (unArg a)
_ -> return v
where
inc w = case ignoreSharing w of
Lit (LitInt r n) -> Lit (LitInt (fuseRange c r) $ n + 1)
_ -> Con c [defaultArg w]
reduceNat v = return v
unfoldDefinition ::
Bool -> (Term -> ReduceM (Blocked Term)) ->
Term -> QName -> Args -> ReduceM (Blocked Term)
unfoldDefinition b keepGoing v f args = snd <$> do
unfoldDefinition' b (\ t -> (NoSimplification,) <$> keepGoing t) v f $
map Apply args
unfoldDefinitionE ::
Bool -> (Term -> ReduceM (Blocked Term)) ->
Term -> QName -> Elims -> ReduceM (Blocked Term)
unfoldDefinitionE b keepGoing v f es = snd <$>
unfoldDefinition' b (\ t -> (NoSimplification,) <$> keepGoing t) v f es
unfoldDefinition' ::
Bool -> (Term -> ReduceM (Simplification, Blocked Term)) ->
Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
unfoldDefinition' unfoldDelayed keepGoing v0 f es =
do
info <- getConstInfo f
allowed <- asks envAllowedReductions
let def = theDef info
v = v0 `applyE` es
dontUnfold =
(defNonterminating info && notElem NonTerminatingReductions allowed)
|| (defDelayed info == Delayed && not unfoldDelayed)
case def of
Constructor{conSrcCon = c} ->
retSimpl $ notBlocked $ Con (c `withRangeOf` f) [] `applyE` es
Primitive{primAbstr = ConcreteDef, primName = x, primClauses = cls} -> do
pf <- fromMaybe __IMPOSSIBLE__ <$> getPrimitive' x
reducePrimitive x v0 f es pf dontUnfold
cls (defCompiled info)
_ -> do
if FunctionReductions `elem` allowed ||
(isJust (isProjection_ def) && ProjectionReductions `elem` allowed)
then
reduceNormalE keepGoing v0 f (map notReduced es)
dontUnfold
(defClauses info) (defCompiled info)
else retSimpl $ notBlocked v
where
retSimpl v = (,v) <$> getSimplification
reducePrimitive x v0 f es pf dontUnfold cls mcc
| genericLength es < ar
= retSimpl $ notBlocked $ v0 `applyE` es
| otherwise = do
let (es1,es2) = genericSplitAt ar es
args1 = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es1
r <- primFunImplementation pf args1
case r of
NoReduction args1' -> do
let es1' = map (fmap Apply) args1'
if null cls then do
retSimpl $ applyE (Def f []) <$> do
traverse id $
map mredToBlocked es1' ++ map notBlocked es2
else
reduceNormalE keepGoing v0 f
(es1' ++ map notReduced es2)
dontUnfold cls mcc
YesReduction simpl v -> performedSimplification' simpl $
keepGoing $ v `applyE` es2
where
ar = primFunArity pf
mredToBlocked :: MaybeReduced a -> Blocked a
mredToBlocked (MaybeRed NotReduced x) = notBlocked x
mredToBlocked (MaybeRed (Reduced b) x) = x <$ b
reduceNormalE :: (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> [MaybeReduced Elim] -> Bool -> [Clause] -> Maybe CompiledClauses -> ReduceM (Simplification, Blocked Term)
reduceNormalE keepGoing v0 f es dontUnfold def mcc = do
case def of
_ | dontUnfold -> defaultResult
[] -> defaultResult
cls -> do
ev <- appDefE_ f v0 cls mcc es
case ev of
NoReduction v -> do
traceSDoc "tc.reduce'" 90 (vcat
[ text "*** tried to reduce' " <+> prettyTCM f
, text " es = " <+> sep (map (prettyTCM . ignoreReduced) es)
, text " stuck on" <+> prettyTCM (ignoreBlocking v) ]) $ do
retSimpl v
YesReduction simpl v -> performedSimplification' simpl $ do
traceSDoc "tc.reduce'" 90 (text "*** reduced definition: " <+> prettyTCM f) $ do
traceSDoc "tc.reduce'" 95 (text " result" <+> prettyTCM v) $ do
traceSDoc "tc.reduce'" 100 (text " raw " <+> text (show v)) $ do
keepGoing v
where defaultResult = retSimpl $ notBlocked $ vfull
vfull = v0 `applyE` map ignoreReduced es
reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)
reduceDefCopy f vs = do
info <- TCM.getConstInfo f
if (defCopy info) then reduceDef_ info f vs else return $ NoReduction ()
where
reduceDef_ :: Definition -> QName -> Args -> TCM (Reduced () Term)
reduceDef_ info f vs = do
let v0 = Def f []
args = map notReduced vs
cls = (defClauses info)
mcc = (defCompiled info)
if (defDelayed info == Delayed) || (defNonterminating info)
then return $ NoReduction ()
else do
ev <- runReduceM $ appDef_ f v0 cls mcc args
case ev of
YesReduction simpl t -> return $ YesReduction simpl t
NoReduction args' -> return $ NoReduction ()
reduceHead :: Term -> TCM (Blocked Term)
reduceHead = runReduceM . reduceHead'
reduceHead' :: Term -> ReduceM (Blocked Term)
reduceHead' v = do
v <- constructorForm v
reportSDoc "tc.inj.reduce" 30 $ text "reduceHead" <+> prettyTCM v
case ignoreSharing v of
Def f es -> do
abstractMode <- envAbstractMode <$> ask
isAbstract <- treatAbstractly f
reportSLn "tc.inj.reduce" 50 $
"reduceHead: we are in " ++ show abstractMode++ "; " ++ show f ++
" is treated " ++ if isAbstract then "abstractly" else "concretely"
let v0 = Def f []
red = unfoldDefinitionE False reduceHead' v0 f es
def <- theDef <$> getConstInfo f
case def of
Function{ funClauses = [ _ ], funDelayed = NotDelayed, funTerminates = Just True } -> do
reportSLn "tc.inj.reduce" 50 $ "reduceHead: head " ++ show f ++ " is Function"
red
Datatype{ dataClause = Just _ } -> red
Record{ recClause = Just _ } -> red
_ -> return $ notBlocked v
_ -> return $ notBlocked v
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef_ f v0 cls mcc args = appDefE_ f v0 cls mcc $ map (fmap Apply) args
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE_ f v0 cls mcc args =
local (\ e -> e { envAppDef = Just f }) $
maybe (appDefE' v0 cls args)
(\cc -> appDefE v0 cc args) mcc
appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef v cc args = appDefE v cc $ map (fmap Apply) args
appDefE :: Term -> CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE v cc es = do
r <- matchCompiledE cc es
case r of
YesReduction simpl t -> return $ YesReduction simpl t
NoReduction es' -> return $ NoReduction $ applyE v <$> es'
appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef' v cls args = appDefE' v cls $ map (fmap Apply) args
appDefE' :: Term -> [Clause] -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE' v cls es = goCls cls $ map ignoreReduced es
where
goCls :: [Clause] -> [Elim] -> ReduceM (Reduced (Blocked Term) Term)
goCls cl es = do
reportSLn "tc.reduce'" 95 $ "Reduce.goCls tries reduction, #clauses = " ++ show (length cl)
let cantReduce es = return $ NoReduction $ notBlocked $ v `applyE` es
case cl of
[] -> cantReduce es
cl @ Clause { clauseBody = body } : cls -> do
let pats = namedClausePats cl
n = length pats
if length es < n then goCls cls es else do
let (es0, es1) = splitAt n es
(m, es0) <- matchCopatterns pats es0
es <- return $ es0 ++ es1
case m of
No -> goCls cls es
DontKnow Nothing -> cantReduce es
DontKnow (Just m) -> return $ NoReduction $ blocked m $ v `applyE` es
Yes simpl vs
| isJust (getBodyUnraised body)
-> return $ YesReduction simpl $
app vs body EmptyS `applyE` es1
| otherwise -> cantReduce es
app :: [Term] -> ClauseBody -> Substitution -> Term
app [] (Body v) sigma = applySubst sigma v
app (v : vs) (Bind (Abs _ b)) sigma = app vs b (v :# sigma)
app (v : vs) (Bind (NoAbs _ b)) sigma = app vs b sigma
app _ NoBody sigma = __IMPOSSIBLE__
app (_ : _) (Body _) sigma = __IMPOSSIBLE__
app [] (Bind _) sigma = __IMPOSSIBLE__
instance Reduce a => Reduce (Closure a) where
reduce' cl = do
x <- enterClosure cl reduce'
return $ cl { clValue = x }
instance Reduce Telescope where
reduce' tel = return tel
instance Reduce Constraint where
reduce' (ValueCmp cmp t u v) = do
(t,u,v) <- reduce' (t,u,v)
return $ ValueCmp cmp t u v
reduce' (ElimCmp cmp t v as bs) =
ElimCmp cmp <$> reduce' t <*> reduce' v <*> reduce' as <*> reduce' bs
reduce' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> reduce' (u,v)
reduce' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> reduce' (a,b)
reduce' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> reduce' (tela,telb)
reduce' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> reduce' (a,b)
reduce' (Guarded c pid) = Guarded <$> reduce' c <*> pure pid
reduce' (UnBlock m) = return $ UnBlock m
reduce' (FindInScope m cands) = FindInScope m <$> mapM reduce' cands
reduce' (IsEmpty r t) = IsEmpty r <$> reduce' t
instance (Ord k, Reduce e) => Reduce (Map k e) where
reduce' = traverse reduce'
class Simplify t where
simplify' :: t -> ReduceM t
instance Simplify Term where
simplify' v = do
v <- instantiate' v
case v of
Def f vs -> do
let keepGoing v = (,NotBlocked v) <$> getSimplification
(simpl, v) <- unfoldDefinition' False keepGoing (Def f []) f vs
reportSDoc "tc.simplify'" 20 $
text ("simplify': unfolding definition returns " ++ show simpl)
<+> prettyTCM (ignoreBlocking v)
case simpl of
YesSimplification -> simplifyBlocked' v
NoSimplification -> Def f <$> simplify' vs
MetaV x vs -> MetaV x <$> simplify' vs
Con c vs -> Con c <$> simplify' vs
Sort s -> sortTm <$> simplify' s
Level l -> levelTm <$> simplify' l
Pi a b -> Pi <$> simplify' a <*> simplify' b
Lit l -> return v
Var i vs -> Var i <$> simplify' vs
Lam h v -> Lam h <$> simplify' v
DontCare v -> dontCare <$> simplify' v
ExtLam{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
simplifyBlocked' (Blocked _ t) = return t
simplifyBlocked' (NotBlocked t) = simplify' t
instance Simplify Type where
simplify' (El s t) = El <$> simplify' s <*> simplify' t
instance Simplify Elim where
simplify' (Apply v) = Apply <$> simplify' v
simplify' (Proj f) = pure $ Proj f
instance Simplify Sort where
simplify' s = do
case s of
DLub s1 s2 -> dLub <$> simplify' s1 <*> simplify' s2
Type s -> levelSort <$> simplify' s
Prop -> return s
Inf -> return s
instance Simplify Level where
simplify' (Max as) = levelMax <$> simplify' as
instance Simplify PlusLevel where
simplify' l@ClosedLevel{} = return l
simplify' (Plus n l) = Plus n <$> simplify' l
instance Simplify LevelAtom where
simplify' l = do
l <- instantiate' l
case l of
MetaLevel m vs -> MetaLevel m <$> simplify' vs
BlockedLevel m v -> BlockedLevel m <$> simplify' v
NeutralLevel v -> NeutralLevel <$> simplify' v
UnreducedLevel v -> UnreducedLevel <$> simplify' v
instance (Subst t, Simplify t) => Simplify (Abs t) where
simplify' a@(Abs x _) = Abs x <$> underAbstraction_ a simplify'
simplify' (NoAbs x v) = NoAbs x <$> simplify' v
instance Simplify t => Simplify (Arg t) where
simplify' = traverse simplify'
instance Simplify t => Simplify (Named name t) where
simplify' = traverse simplify'
instance Simplify t => Simplify (Dom t) where
simplify' = traverse simplify'
instance Simplify t => Simplify [t] where
simplify' = traverse simplify'
instance (Ord k, Simplify e) => Simplify (Map k e) where
simplify' = traverse simplify'
instance Simplify a => Simplify (Maybe a) where
simplify' = traverse simplify'
instance (Simplify a, Simplify b) => Simplify (a,b) where
simplify' (x,y) = (,) <$> simplify' x <*> simplify' y
instance (Simplify a, Simplify b, Simplify c) => Simplify (a,b,c) where
simplify' (x,y,z) =
do (x,(y,z)) <- simplify' (x,(y,z))
return (x,y,z)
instance Simplify a => Simplify (Closure a) where
simplify' cl = do
x <- enterClosure cl simplify'
return $ cl { clValue = x }
instance (Subst a, Simplify a) => Simplify (Tele a) where
simplify' EmptyTel = return EmptyTel
simplify' (ExtendTel a b) = uncurry ExtendTel <$> simplify' (a, b)
instance Simplify ProblemConstraint where
simplify' (PConstr pid c) = PConstr pid <$> simplify' c
instance Simplify Constraint where
simplify' (ValueCmp cmp t u v) = do
(t,u,v) <- simplify' (t,u,v)
return $ ValueCmp cmp t u v
simplify' (ElimCmp cmp t v as bs) =
ElimCmp cmp <$> simplify' t <*> simplify' v <*> simplify' as <*> simplify' bs
simplify' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> simplify' (u,v)
simplify' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> simplify' (a,b)
simplify' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> simplify' (tela,telb)
simplify' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> simplify' (a,b)
simplify' (Guarded c pid) = Guarded <$> simplify' c <*> pure pid
simplify' (UnBlock m) = return $ UnBlock m
simplify' (FindInScope m cands) = FindInScope m <$> mapM simplify' cands
simplify' (IsEmpty r t) = IsEmpty r <$> simplify' t
instance Simplify Bool where
simplify' = return
instance Simplify Pattern where
simplify' p = case p of
VarP _ -> return p
LitP _ -> return p
ConP c mt ps -> ConP c <$> simplify' mt <*> simplify' ps
DotP v -> DotP <$> simplify' v
ProjP _ -> return p
instance Simplify ClauseBody where
simplify' (Body t) = Body <$> simplify' t
simplify' (Bind b) = Bind <$> simplify' b
simplify' NoBody = return NoBody
instance Simplify DisplayForm where
simplify' (Display n ps v) = Display n <$> simplify' ps <*> return v
class Normalise t where
normalise' :: t -> ReduceM t
instance Normalise Sort where
normalise' s = do
s <- reduce' s
case s of
DLub s1 s2 -> dLub <$> normalise' s1 <*> normalise' s2
Prop -> return s
Type s -> levelSort <$> normalise' s
Inf -> return Inf
instance Normalise Type where
normalise' (El s t) = El <$> normalise' s <*> normalise' t
instance Normalise Term where
normalise' v =
do v <- reduce' v
case v of
Var n vs -> Var n <$> normalise' vs
Con c vs -> Con c <$> normalise' vs
Def f vs -> Def f <$> normalise' vs
MetaV x vs -> MetaV x <$> normalise' vs
Lit _ -> return v
Level l -> levelTm <$> normalise' l
Lam h b -> Lam h <$> normalise' b
Sort s -> sortTm <$> normalise' s
Pi a b -> uncurry Pi <$> normalise' (a,b)
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
DontCare _ -> return v
instance Normalise Elim where
normalise' (Apply v) = Apply <$> normalise' v
normalise' (Proj f) = pure $ Proj f
instance Normalise Level where
normalise' (Max as) = levelMax <$> normalise' as
instance Normalise PlusLevel where
normalise' l@ClosedLevel{} = return l
normalise' (Plus n l) = Plus n <$> normalise' l
instance Normalise LevelAtom where
normalise' l = do
l <- reduce' l
case l of
MetaLevel m vs -> MetaLevel m <$> normalise' vs
BlockedLevel m v -> BlockedLevel m <$> normalise' v
NeutralLevel v -> NeutralLevel <$> normalise' v
UnreducedLevel{} -> __IMPOSSIBLE__
instance Normalise ClauseBody where
normalise' (Body t) = Body <$> normalise' t
normalise' (Bind b) = Bind <$> normalise' b
normalise' NoBody = return NoBody
instance (Subst t, Normalise t) => Normalise (Abs t) where
normalise' a@(Abs x _) = Abs x <$> underAbstraction_ a normalise'
normalise' (NoAbs x v) = NoAbs x <$> normalise' v
instance Normalise t => Normalise (Arg t) where
normalise' a | isIrrelevant a = return a
| otherwise = traverse normalise' a
instance Normalise t => Normalise (Named name t) where
normalise' = traverse normalise'
instance Normalise t => Normalise (Dom t) where
normalise' = traverse normalise'
instance Normalise t => Normalise [t] where
normalise' = traverse normalise'
instance (Normalise a, Normalise b) => Normalise (a,b) where
normalise' (x,y) = (,) <$> normalise' x <*> normalise' y
instance (Normalise a, Normalise b, Normalise c) => Normalise (a,b,c) where
normalise' (x,y,z) =
do (x,(y,z)) <- normalise' (x,(y,z))
return (x,y,z)
instance Normalise a => Normalise (Closure a) where
normalise' cl = do
x <- enterClosure cl normalise'
return $ cl { clValue = x }
instance (Subst a, Normalise a) => Normalise (Tele a) where
normalise' EmptyTel = return EmptyTel
normalise' (ExtendTel a b) = uncurry ExtendTel <$> normalise' (a, b)
instance Normalise ProblemConstraint where
normalise' (PConstr pid c) = PConstr pid <$> normalise' c
instance Normalise Constraint where
normalise' (ValueCmp cmp t u v) = do
(t,u,v) <- normalise' (t,u,v)
return $ ValueCmp cmp t u v
normalise' (ElimCmp cmp t v as bs) =
ElimCmp cmp <$> normalise' t <*> normalise' v <*> normalise' as <*> normalise' bs
normalise' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> normalise' (u,v)
normalise' (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> normalise' (a,b)
normalise' (TelCmp a b cmp tela telb) = uncurry (TelCmp a b cmp) <$> normalise' (tela,telb)
normalise' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> normalise' (a,b)
normalise' (Guarded c pid) = Guarded <$> normalise' c <*> pure pid
normalise' (UnBlock m) = return $ UnBlock m
normalise' (FindInScope m cands) = FindInScope m <$> mapM normalise' cands
normalise' (IsEmpty r t) = IsEmpty r <$> normalise' t
instance Normalise Bool where
normalise' = return
instance Normalise Pattern where
normalise' p = case p of
VarP _ -> return p
LitP _ -> return p
ConP c mt ps -> ConP c <$> normalise' mt <*> normalise' ps
DotP v -> DotP <$> normalise' v
ProjP _ -> return p
instance Normalise DisplayForm where
normalise' (Display n ps v) = Display n <$> normalise' ps <*> return v
instance (Ord k, Normalise e) => Normalise (Map k e) where
normalise' = traverse normalise'
instance Normalise a => Normalise (Maybe a) where
normalise' = traverse normalise'
class InstantiateFull t where
instantiateFull' :: t -> ReduceM t
instance InstantiateFull Name where
instantiateFull' = return
instance InstantiateFull Sort where
instantiateFull' s = do
s <- instantiate' s
case s of
Type n -> levelSort <$> instantiateFull' n
Prop -> return s
DLub s1 s2 -> dLub <$> instantiateFull' s1 <*> instantiateFull' s2
Inf -> return s
instance InstantiateFull Type where
instantiateFull' (El s t) =
El <$> instantiateFull' s <*> instantiateFull' t
instance InstantiateFull Term where
instantiateFull' v = etaOnce =<< do
v <- instantiate' v
case v of
Var n vs -> Var n <$> instantiateFull' vs
Con c vs -> Con c <$> instantiateFull' vs
Def f vs -> Def f <$> instantiateFull' vs
MetaV x vs -> MetaV x <$> instantiateFull' vs
Lit _ -> return v
Level l -> levelTm <$> instantiateFull' l
Lam h b -> Lam h <$> instantiateFull' b
Sort s -> sortTm <$> instantiateFull' s
Pi a b -> uncurry Pi <$> instantiateFull' (a,b)
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
DontCare v -> dontCare <$> instantiateFull' v
instance InstantiateFull Level where
instantiateFull' (Max as) = levelMax <$> instantiateFull' as
instance InstantiateFull PlusLevel where
instantiateFull' l@ClosedLevel{} = return l
instantiateFull' (Plus n l) = Plus n <$> instantiateFull' l
instance InstantiateFull LevelAtom where
instantiateFull' l = case l of
MetaLevel m vs -> do
v <- instantiateFull' (MetaV m vs)
case ignoreSharing v of
MetaV m vs -> return $ MetaLevel m vs
_ -> return $ UnreducedLevel v
NeutralLevel v -> NeutralLevel <$> instantiateFull' v
BlockedLevel m v ->
ifM (isInstantiatedMeta m)
(UnreducedLevel <$> instantiateFull' v)
(BlockedLevel m <$> instantiateFull' v)
UnreducedLevel v -> UnreducedLevel <$> instantiateFull' v
instance InstantiateFull Bool where
instantiateFull' = return
instance InstantiateFull Pattern where
instantiateFull' v@VarP{} = return v
instantiateFull' (DotP t) = DotP <$> instantiateFull' t
instantiateFull' (ConP n mt ps) = ConP n <$> instantiateFull' mt <*> instantiateFull' ps
instantiateFull' l@LitP{} = return l
instantiateFull' p@ProjP{} = return p
instance InstantiateFull ClauseBody where
instantiateFull' (Body t) = Body <$> instantiateFull' t
instantiateFull' (Bind b) = Bind <$> instantiateFull' b
instantiateFull' NoBody = return NoBody
instance (Subst t, InstantiateFull t) => InstantiateFull (Abs t) where
instantiateFull' a@(Abs x _) = Abs x <$> underAbstraction_ a instantiateFull'
instantiateFull' (NoAbs x a) = NoAbs x <$> instantiateFull' a
instance InstantiateFull t => InstantiateFull (Arg t) where
instantiateFull' = traverse instantiateFull'
instance InstantiateFull t => InstantiateFull (Named name t) where
instantiateFull' = traverse instantiateFull'
instance InstantiateFull t => InstantiateFull (Dom t) where
instantiateFull' = traverse instantiateFull'
instance InstantiateFull t => InstantiateFull [t] where
instantiateFull' = traverse instantiateFull'
instance (InstantiateFull a, InstantiateFull b) => InstantiateFull (a,b) where
instantiateFull' (x,y) = (,) <$> instantiateFull' x <*> instantiateFull' y
instance (InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a,b,c) where
instantiateFull' (x,y,z) =
do (x,(y,z)) <- instantiateFull' (x,(y,z))
return (x,y,z)
instance InstantiateFull a => InstantiateFull (Closure a) where
instantiateFull' cl = do
x <- enterClosure cl instantiateFull'
return $ cl { clValue = x }
instance InstantiateFull ProblemConstraint where
instantiateFull' (PConstr p c) = PConstr p <$> instantiateFull' c
instance InstantiateFull Constraint where
instantiateFull' c = case c of
ValueCmp cmp t u v -> do
(t,u,v) <- instantiateFull' (t,u,v)
return $ ValueCmp cmp t u v
ElimCmp cmp t v as bs ->
ElimCmp cmp <$> instantiateFull' t <*> instantiateFull' v <*> instantiateFull' as <*> instantiateFull' bs
LevelCmp cmp u v -> uncurry (LevelCmp cmp) <$> instantiateFull' (u,v)
TypeCmp cmp a b -> uncurry (TypeCmp cmp) <$> instantiateFull' (a,b)
TelCmp a b cmp tela telb -> uncurry (TelCmp a b cmp) <$> instantiateFull' (tela,telb)
SortCmp cmp a b -> uncurry (SortCmp cmp) <$> instantiateFull' (a,b)
Guarded c pid -> Guarded <$> instantiateFull' c <*> pure pid
UnBlock m -> return $ UnBlock m
FindInScope m cands -> FindInScope m <$> mapM instantiateFull' cands
IsEmpty r t -> IsEmpty r <$> instantiateFull' t
instance InstantiateFull Elim where
instantiateFull' (Apply v) = Apply <$> instantiateFull' v
instantiateFull' (Proj f) = pure $ Proj f
instance (Ord k, InstantiateFull e) => InstantiateFull (Map k e) where
instantiateFull' = traverse instantiateFull'
instance (Eq k, Hashable k, InstantiateFull e) => InstantiateFull (HashMap k e) where
instantiateFull' = traverse instantiateFull'
instance InstantiateFull ModuleName where
instantiateFull' = return
instance InstantiateFull Scope where
instantiateFull' = return
instance InstantiateFull Signature where
instantiateFull' (Sig a b) = uncurry Sig <$> instantiateFull' (a, b)
instance InstantiateFull Section where
instantiateFull' (Section tel n) = flip Section n <$> instantiateFull' tel
instance (Subst a, InstantiateFull a) => InstantiateFull (Tele a) where
instantiateFull' EmptyTel = return EmptyTel
instantiateFull' (ExtendTel a b) = uncurry ExtendTel <$> instantiateFull' (a, b)
instance InstantiateFull Char where
instantiateFull' = return
instance InstantiateFull Definition where
instantiateFull' (Defn rel x t pol occ df i c rew inst d) = do
(t, (df, d, rew)) <- instantiateFull' (t, (df, d, rew))
return $ Defn rel x t pol occ df i c rew inst d
instance InstantiateFull RewriteRule where
instantiateFull' (RewriteRule q gamma lhs rhs t) =
RewriteRule q
<$> instantiateFull' gamma
<*> instantiateFull' lhs
<*> instantiateFull' rhs
<*> instantiateFull' t
instance InstantiateFull a => InstantiateFull (Open a) where
instantiateFull' (OpenThing n a) = OpenThing n <$> instantiateFull' a
instance InstantiateFull DisplayForm where
instantiateFull' (Display n ps v) = uncurry (Display n) <$> instantiateFull' (ps, v)
instance InstantiateFull DisplayTerm where
instantiateFull' (DTerm v) = DTerm <$> instantiateFull' v
instantiateFull' (DDot v) = DDot <$> instantiateFull' v
instantiateFull' (DCon c vs) = DCon c <$> instantiateFull' vs
instantiateFull' (DDef c vs) = DDef c <$> instantiateFull' vs
instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws)
instance InstantiateFull Defn where
instantiateFull' d = case d of
Axiom{} -> return d
Function{ funClauses = cs, funCompiled = cc, funInv = inv } -> do
(cs, cc, inv) <- instantiateFull' (cs, cc, inv)
return $ d { funClauses = cs, funCompiled = cc, funInv = inv }
Datatype{ dataSort = s, dataClause = cl } -> do
s <- instantiateFull' s
cl <- instantiateFull' cl
return $ d { dataSort = s, dataClause = cl }
Record{ recConType = t, recClause = cl, recTel = tel } -> do
t <- instantiateFull' t
cl <- instantiateFull' cl
tel <- instantiateFull' tel
return $ d { recConType = t, recClause = cl, recTel = tel }
Constructor{} -> return d
Primitive{ primClauses = cs } -> do
cs <- instantiateFull' cs
return $ d { primClauses = cs }
instance InstantiateFull FunctionInverse where
instantiateFull' NotInjective = return NotInjective
instantiateFull' (Inverse inv) = Inverse <$> instantiateFull' inv
instance InstantiateFull a => InstantiateFull (WithArity a) where
instantiateFull' (WithArity n a) = WithArity n <$> instantiateFull' a
instance InstantiateFull a => InstantiateFull (Case a) where
instantiateFull' (Branches cs ls m) =
Branches <$> instantiateFull' cs
<*> instantiateFull' ls
<*> instantiateFull' m
instance InstantiateFull CompiledClauses where
instantiateFull' Fail = return Fail
instantiateFull' (Done m t) = Done m <$> instantiateFull' t
instantiateFull' (Case n bs) = Case n <$> instantiateFull' bs
instance InstantiateFull Clause where
instantiateFull' (Clause r tel perm ps b t) =
Clause r <$> instantiateFull' tel
<*> return perm
<*> instantiateFull' ps
<*> instantiateFull' b
<*> instantiateFull' t
instance InstantiateFull Interface where
instantiateFull' (Interface h ms mod scope inside
sig b hsImports highlighting pragmas patsyns) =
Interface h ms mod scope inside
<$> instantiateFull' sig
<*> instantiateFull' b
<*> return hsImports
<*> return highlighting
<*> return pragmas
<*> return patsyns
instance InstantiateFull a => InstantiateFull (Builtin a) where
instantiateFull' (Builtin t) = Builtin <$> instantiateFull' t
instantiateFull' (Prim x) = Prim <$> instantiateFull' x
instance InstantiateFull QName where
instantiateFull' = return
instance InstantiateFull a => InstantiateFull (Maybe a) where
instantiateFull' = mapM instantiateFull'