{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Reduce where
import Prelude hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import qualified Data.List as List
import Data.List ((\\))
import Data.Maybe
import Data.Map (Map)
import Data.Traversable
import Data.Hashable
import Agda.Interaction.Options
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Scope.Base (Scope)
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad hiding ( underAbstraction_, enterClosure, isInstantiatedMeta
, 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.Reduce.Monad
import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Match
import {-# SOURCE #-} Agda.TypeChecking.Patterns.Match
import {-# SOURCE #-} Agda.TypeChecking.Pretty
import {-# SOURCE #-} Agda.TypeChecking.Rewriting
import {-# SOURCE #-} Agda.TypeChecking.Reduce.Fast
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.HashMap (HashMap)
import Agda.Utils.Size
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'
isFullyInstantiatedMeta :: MetaId -> TCM Bool
isFullyInstantiatedMeta m = do
mv <- TCM.lookupMeta m
case mvInstantiation mv of
InstV _tel v -> null . allMetas <$> instantiateFull v
_ -> return False
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
instantiate' (Level l) = levelTm <$> instantiate' l
instantiate' (Sort s) = Sort <$> instantiate' s
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 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
instance Instantiate Type where
instantiate' (El s t) = El <$> instantiate' s <*> instantiate' t
instance Instantiate Sort where
instantiate' s = case s of
MetaS x es -> instantiate' (MetaV x es) >>= \case
Sort s' -> return s'
MetaV x' es' -> return $ MetaS x' es'
_ -> __IMPOSSIBLE__
_ -> return s
instance Instantiate Elim where
instantiate' (Apply v) = Apply <$> instantiate' v
instantiate' (Proj o f)= pure $ Proj o 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' EmptyTel = return EmptyTel
instantiate' (ExtendTel a tel) = ExtendTel <$> instantiate' a <*> instantiate' 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 fs t v as bs) =
ElimCmp cmp fs <$> 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 b args) = FindInScope m b <$> mapM instantiate' args
instantiate' (IsEmpty r t) = IsEmpty r <$> instantiate' t
instantiate' (CheckSizeLtSat t) = CheckSizeLtSat <$> instantiate' t
instantiate' c@CheckFunDef{} = return c
instantiate' (HasBiggerSort a) = HasBiggerSort <$> instantiate' a
instantiate' (HasPTSRule a b) = uncurry HasPTSRule <$> instantiate' (a,b)
instance Instantiate e => Instantiate (Map k e) where
instantiate' = traverse instantiate'
instance Instantiate Candidate where
instantiate' (Candidate u t eti ov) = Candidate <$> instantiate' u <*> instantiate' t <*> pure eti <*> pure ov
instance Instantiate EqualityView where
instantiate' (OtherType t) = OtherType
<$> instantiate' t
instantiate' (EqualityType s eq l t a b) = EqualityType
<$> instantiate' s
<*> return eq
<*> mapM instantiate' l
<*> instantiate' t
<*> instantiate' a
<*> instantiate' b
ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (NotBlocked -> Term -> tcm a) -> tcm a
ifBlocked t blocked unblocked = do
t <- liftTCM $ reduceB t
case t of
Blocked m _ -> blocked m (ignoreBlocking t)
NotBlocked _ (MetaV m _) -> blocked m (ignoreBlocking t)
NotBlocked nb _ -> unblocked nb (ignoreBlocking t)
isBlocked :: MonadTCM tcm => Term -> tcm (Maybe MetaId)
isBlocked t = ifBlocked t (\m _ -> return $ Just m) (\_ _ -> return Nothing)
ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (NotBlocked -> Type -> tcm a) -> tcm a
ifBlockedType (El s t) blocked unblocked =
ifBlocked t (\ m v -> blocked m $ El s v) (\ nb v -> unblocked nb $ El s v)
isBlockedType :: MonadTCM tcm => Type -> tcm (Maybe MetaId)
isBlockedType t = ifBlockedType t (\m _ -> return $ Just m) (\_ _ -> return Nothing)
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 = {-# SCC "reduce'<Sort>" #-}
ifNotM hasUniversePolymorphism (red s) $ red =<< instantiateFull' s
where
red s = do
s <- instantiate' s
case s of
PiSort s1 s2 -> do
(s1,s2) <- reduce' (s1,s2)
maybe (return $ PiSort s1 s2) reduce' $ piSort' s1 s2
UnivSort s' -> do
s' <- reduce' s'
maybe (return $ UnivSort s') reduce' $ univSort' s'
Prop -> return s
Type s' -> Type <$> reduce' s'
Inf -> return Inf
SizeUniv -> return SizeUniv
MetaS x es -> return s
instance Reduce Elim where
reduce' (Apply v) = Apply <$> reduce' v
reduce' (Proj o f)= pure $ Proj o 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 r v -> return $ NotBlocked r $ NeutralLevel r 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 bv of
NotBlocked r (MetaV m vs) -> return $ NotBlocked r $ MetaLevel m vs
Blocked m _ -> return $ Blocked m $ BlockedLevel m v
NotBlocked r _ -> return $ NotBlocked r $ NeutralLevel r v
instance (Subst t a, Reduce a) => Reduce (Abs a) 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' = {-# SCC "reduce'<Term>" #-} maybeFastReduceTerm
shouldTryFastReduce :: ReduceM Bool
shouldTryFastReduce = do
allowed <- asks envAllowedReductions
let optionalReductions = [NonTerminatingReductions, UnconfirmedReductions]
requiredReductions = allReductions \\ optionalReductions
return $ (allowed \\ optionalReductions) == requiredReductions
maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)
maybeFastReduceTerm v = do
let tryFast = case v of
Def{} -> True
Con{} -> True
MetaV{} -> True
_ -> False
if not tryFast then slowReduceTerm v
else
case v of
MetaV x _ -> ifM (isOpen x) (return $ notBlocked v) (maybeFast v)
_ -> maybeFast v
where
isOpen x = isOpenMeta . mvInstantiation <$> lookupMeta x
maybeFast v = ifM shouldTryFastReduce (fastReduce v) (slowReduceTerm v)
slowReduceTerm :: Term -> ReduceM (Blocked Term)
slowReduceTerm 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 ci es -> do
let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
v <- unfoldDefinition False reduceB' (Con c ci []) (conName c) args
traverse reduceNat v
Sort s -> fmap Sort <$> reduceB' s
Level l -> ifM (elem LevelReductions <$> asks envAllowedReductions)
(fmap levelTm <$> reduceB' l)
done
Pi _ _ -> done
Lit _ -> done
Var _ _ -> done
Lam _ _ -> done
DontCare _ -> done
where
reduceNat v@(Con c ci []) = do
mz <- getBuiltin' builtinZero
case v of
_ | Just v == mz -> return $ Lit $ LitNat (getRange c) 0
_ -> return v
reduceNat v@(Con c ci [Apply a]) | visible a && isRelevant a = do
ms <- getBuiltin' builtinSuc
case v of
_ | Just (Con c ci []) == ms -> inc <$> reduce' (unArg a)
_ -> return v
where
inc w = case w of
Lit (LitNat r n) -> Lit (LitNat (fuseRange c r) $ n + 1)
_ -> Con c ci [Apply $ defaultArg w]
reduceNat v = return v
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
unfoldCorecursionE (Proj o p) = notBlocked . Proj o <$> getOriginalProjection p
unfoldCorecursionE (Apply (Arg info v)) = fmap (Apply . Arg info) <$>
unfoldCorecursion v
unfoldCorecursion :: Term -> ReduceM (Blocked Term)
unfoldCorecursion v = do
v <- instantiate' v
case v of
Def f es -> unfoldDefinitionE True unfoldCorecursion (Def f []) f es
_ -> slowReduceTerm v
unfoldDefinition ::
Bool -> (Term -> ReduceM (Blocked Term)) ->
Term -> QName -> Args -> ReduceM (Blocked Term)
unfoldDefinition unfoldDelayed keepGoing v f args =
unfoldDefinitionE unfoldDelayed keepGoing v f (map Apply args)
unfoldDefinitionE ::
Bool -> (Term -> ReduceM (Blocked Term)) ->
Term -> QName -> Elims -> ReduceM (Blocked Term)
unfoldDefinitionE unfoldDelayed keepGoing v f es = do
r <- unfoldDefinitionStep unfoldDelayed v f es
case r of
NoReduction v -> return v
YesReduction _ v -> keepGoing v
unfoldDefinition' ::
Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) ->
Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
unfoldDefinition' unfoldDelayed keepGoing v0 f es = do
r <- unfoldDefinitionStep unfoldDelayed v0 f es
case r of
NoReduction v -> return (NoSimplification, v)
YesReduction simp v -> keepGoing simp v
unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep unfoldDelayed v0 f es =
{-# SCC "reduceDef" #-} do
info <- getConstInfo f
rewr <- instantiateRewriteRules =<< getRewriteRulesFor f
allowed <- asks envAllowedReductions
let def = theDef info
v = v0 `applyE` es
dontUnfold =
(defNonterminating info && notElem NonTerminatingReductions allowed)
|| (defTerminationUnconfirmed info && notElem UnconfirmedReductions allowed)
|| (defDelayed info == Delayed && not unfoldDelayed)
copatterns =
case def of
Function{funCopatternLHS = b} -> b
_ -> False
case def of
Constructor{conSrcCon = c} ->
noReduction $ notBlocked $ Con (c `withRangeOf` f) ConOSystem [] `applyE` es
Primitive{primAbstr = ConcreteDef, primName = x, primClauses = cls} -> do
pf <- fromMaybe __IMPOSSIBLE__ <$> getPrimitive' x
if FunctionReductions `elem` allowed
then reducePrimitive x v0 f es pf dontUnfold
cls (defCompiled info) rewr
else noReduction $ notBlocked v
_ -> do
if (RecursiveReductions `elem` allowed) ||
(isJust (isProjection_ def) && ProjectionReductions `elem` allowed) ||
(isInlineFun def && InlineReductions `elem` allowed) ||
(definitelyNonRecursive_ def && copatterns && CopatternReductions `elem` allowed) ||
(definitelyNonRecursive_ def && FunctionReductions `elem` allowed)
then
reduceNormalE v0 f (map notReduced es) dontUnfold
(defClauses info) (defCompiled info) rewr
else noReduction $ notBlocked v
where
noReduction = return . NoReduction
yesReduction s = return . YesReduction s
reducePrimitive x v0 f es pf dontUnfold cls mcc rewr
| length es < ar
= noReduction $ NotBlocked Underapplied $ v0 `applyE` es
| otherwise = {-# SCC "reducePrimitive" #-} do
let (es1,es2) = splitAt 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
noReduction $ applyE (Def f []) <$> do
traverse id $
map mredToBlocked es1' ++ map notBlocked es2
else
reduceNormalE v0 f (es1' ++ map notReduced es2) dontUnfold cls mcc rewr
YesReduction simpl v -> yesReduction simpl $ 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 -> QName -> [MaybeReduced Elim] -> Bool -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> ReduceM (Reduced (Blocked Term) Term)
reduceNormalE v0 f es dontUnfold def mcc rewr = {-# SCC "reduceNormal" #-} do
case (def,rewr) of
_ | dontUnfold -> defaultResult
([],[]) -> defaultResult
(cls,rewr) -> do
ev <- appDefE_ f v0 cls mcc rewr es
debugReduce ev
return ev
where
defaultResult = noReduction $ NotBlocked ReallyNotBlocked vfull
vfull = v0 `applyE` map ignoreReduced es
debugReduce ev = verboseS "tc.reduce" 90 $ do
case ev of
NoReduction v -> do
reportSDoc "tc.reduce" 90 $ vcat
[ text "*** tried to reduce " <+> prettyTCM f
, text " es = " <+> sep (map (prettyTCM . ignoreReduced) es)
, text " stuck on" <+> prettyTCM (ignoreBlocking v)
]
YesReduction _simpl v -> do
reportSDoc "tc.reduce" 90 $ text "*** reduced definition: " <+> prettyTCM f
reportSDoc "tc.reduce" 95 $ text " result" <+> prettyTCM v
reportSDoc "tc.reduce" 100 $ text " raw " <+> text (show v)
reduceDefCopy :: QName -> Elims -> TCM (Reduced () Term)
reduceDefCopy f es = do
info <- TCM.getConstInfo f
rewr <- instantiateRewriteRules =<< TCM.getRewriteRulesFor f
if (defCopy info) then reduceDef_ info rewr f es else return $ NoReduction ()
where
reduceDef_ :: Definition -> RewriteRules -> QName -> Elims -> TCM (Reduced () Term)
reduceDef_ info rewr f es = do
let v0 = Def f []
cls = (defClauses info)
mcc = (defCompiled info)
if (defDelayed info == Delayed) || (defNonterminating info)
then return $ NoReduction ()
else do
ev <- runReduceM $ appDefE_ f v0 cls mcc rewr $ map notReduced es
case ev of
YesReduction simpl t -> return $ YesReduction simpl t
NoReduction{} -> return $ NoReduction ()
reduceHead :: Term -> TCM (Blocked Term)
reduceHead = runReduceM . reduceHead'
reduceHead' :: Term -> ReduceM (Blocked Term)
reduceHead' v = do
v <- constructorForm v
traceSDoc "tc.inj.reduce" 30 (text "reduceHead" <+> prettyTCM v) $ do
case v of
Def f es -> do
abstractMode <- envAbstractMode <$> ask
isAbstract <- treatAbstractly f
traceSLn "tc.inj.reduce" 50 (
"reduceHead: we are in " ++ show abstractMode++ "; " ++ show f ++
" is treated " ++ if isAbstract then "abstractly" else "concretely"
) $ do
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
traceSLn "tc.inj.reduce" 50 ("reduceHead: head " ++ show f ++ " is Function") $ do
red
Datatype{ dataClause = Just _ } -> red
Record{ recClause = Just _ } -> red
_ -> return $ notBlocked v
_ -> return $ notBlocked v
unfoldInlined :: Term -> TCM Term
unfoldInlined = runReduceM . unfoldInlined'
unfoldInlined' :: Term -> ReduceM Term
unfoldInlined' v = do
inTypes <- view eWorkingOnTypes
case v of
_ | inTypes -> return v
Def f es -> do
def <- theDef <$> getConstInfo f
case def of
Function{ funCompiled = Just Done{}, funDelayed = NotDelayed }
| def ^. funInline ->
ignoreBlocking <$> unfoldDefinitionE False (return . notBlocked) (Def f []) f es
_ -> return v
_ -> return v
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef_ f v0 cls mcc rewr args = appDefE_ f v0 cls mcc rewr $ map (fmap Apply) args
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE_ f v0 cls mcc rewr args =
local (\ e -> e { envAppDef = Just f }) $
maybe (appDefE' v0 cls rewr args)
(\cc -> appDefE v0 cc rewr args) mcc
appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef v cc rewr args = appDefE v cc rewr $ map (fmap Apply) args
appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE v cc rewr es = do
r <- matchCompiledE cc es
case r of
YesReduction simpl t -> return $ YesReduction simpl t
NoReduction es' -> rewrite (void es') v rewr (ignoreBlocking es')
appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
appDef' v cls rewr args = appDefE' v cls rewr $ map (fmap Apply) args
appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDefE' v cls rewr es = goCls cls $ map ignoreReduced es
where
goCls :: [Clause] -> [Elim] -> ReduceM (Reduced (Blocked Term) Term)
goCls cl es = do
case cl of
[] -> rewrite (NotBlocked MissingClauses ()) v rewr es
cl : cls -> do
let pats = namedClausePats cl
body = clauseBody cl
npats = length pats
nvars = size $ clauseTel cl
if length es < npats then goCls cls es else do
let (es0, es1) = splitAt npats es
(m, es0) <- matchCopatterns pats es0
es <- return $ es0 ++ es1
case m of
No -> goCls cls es
DontKnow b -> rewrite b v rewr es
Yes simpl vs
| Just w <- body -> do
let sigma = buildSubstitution __IMPOSSIBLE__ nvars vs
return $ YesReduction simpl $ applySubst sigma w `applyE` es1
| otherwise -> rewrite (NotBlocked AbsurdMatch ()) v rewr es
instance Reduce a => Reduce (Closure a) where
reduce' cl = do
x <- enterClosure cl reduce'
return $ cl { clValue = x }
instance Reduce Telescope where
reduce' EmptyTel = return EmptyTel
reduce' (ExtendTel a tel) = ExtendTel <$> reduce' a <*> reduce' 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 fs t v as bs) =
ElimCmp cmp fs <$> 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 b cands) = FindInScope m b <$> mapM reduce' cands
reduce' (IsEmpty r t) = IsEmpty r <$> reduce' t
reduce' (CheckSizeLtSat t) = CheckSizeLtSat <$> reduce' t
reduce' c@CheckFunDef{} = return c
reduce' (HasBiggerSort a) = HasBiggerSort <$> reduce' a
reduce' (HasPTSRule a b) = uncurry HasPTSRule <$> reduce' (a,b)
instance Reduce e => Reduce (Map k e) where
reduce' = traverse reduce'
instance Reduce Candidate where
reduce' (Candidate u t eti ov) = Candidate <$> reduce' u <*> reduce' t <*> pure eti <*> pure ov
instance Reduce EqualityView where
reduce' (OtherType t) = OtherType
<$> reduce' t
reduce' (EqualityType s eq l t a b) = EqualityType
<$> reduce' s
<*> return eq
<*> mapM reduce' l
<*> reduce' t
<*> reduce' a
<*> reduce' b
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 simp v = return (simp, notBlocked v)
(simpl, v) <- unfoldDefinition' False keepGoing (Def f []) f vs
traceSDoc "tc.simplify'" 90 (
text ("simplify': unfolding definition returns " ++ show simpl)
<+> prettyTCM (ignoreBlocking v)) $ do
case simpl of
YesSimplification -> simplifyBlocked' v
NoSimplification -> Def f <$> simplify' vs
MetaV x vs -> MetaV x <$> simplify' vs
Con c ci vs-> Con c ci <$> simplify' vs
Sort s -> Sort <$> 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
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 o f)= pure $ Proj o f
instance Simplify Sort where
simplify' s = do
case s of
PiSort s1 s2 -> piSort <$> simplify' s1 <*> simplify' s2
UnivSort s -> univSort <$> simplify' s
Type s -> Type <$> simplify' s
Prop -> return s
Inf -> return s
SizeUniv -> return s
MetaS x es -> MetaS x <$> simplify' es
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 r v -> NeutralLevel r <$> simplify' v
UnreducedLevel v -> UnreducedLevel <$> simplify' v
instance (Subst t a, Simplify a) => Simplify (Abs a) 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 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 t 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 fs t v as bs) =
ElimCmp cmp fs <$> 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 b cands) = FindInScope m b <$> mapM simplify' cands
simplify' (IsEmpty r t) = IsEmpty r <$> simplify' t
simplify' (CheckSizeLtSat t) = CheckSizeLtSat <$> simplify' t
simplify' c@CheckFunDef{} = return c
simplify' (HasBiggerSort a) = HasBiggerSort <$> simplify' a
simplify' (HasPTSRule a b) = uncurry HasPTSRule <$> simplify' (a,b)
instance Simplify Bool where
simplify' = return
instance Simplify DisplayForm where
simplify' (Display n ps v) = Display n <$> simplify' ps <*> return v
instance Simplify Candidate where
simplify' (Candidate u t eti ov) = Candidate <$> simplify' u <*> simplify' t <*> pure eti <*> pure ov
instance Simplify EqualityView where
simplify' (OtherType t) = OtherType
<$> simplify' t
simplify' (EqualityType s eq l t a b) = EqualityType
<$> simplify' s
<*> return eq
<*> mapM simplify' l
<*> simplify' t
<*> simplify' a
<*> simplify' b
class Normalise t where
normalise' :: t -> ReduceM t
instance Normalise Sort where
normalise' s = do
s <- reduce' s
case s of
PiSort s1 s2 -> piSort <$> normalise' s1 <*> normalise' s2
UnivSort s -> univSort <$> normalise' s
Prop -> return s
Type s -> Type <$> normalise' s
Inf -> return Inf
SizeUniv -> return SizeUniv
MetaS x es -> return s
instance Normalise Type where
normalise' (El s t) = El <$> normalise' s <*> normalise' t
instance Normalise Term where
normalise' v = ifM shouldTryFastReduce (fastNormalise v) (slowNormaliseArgs =<< reduce' v)
slowNormaliseArgs :: Term -> ReduceM Term
slowNormaliseArgs v = case v of
Var n vs -> Var n <$> normalise' vs
Con c ci vs -> Con c ci <$> 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 -> Sort <$> normalise' s
Pi a b -> uncurry Pi <$> normalise' (a, b)
DontCare _ -> return v
instance Normalise Elim where
normalise' (Apply v) = Apply <$> normalise' v
normalise' (Proj o f)= pure $ Proj o 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 r v -> NeutralLevel r <$> normalise' v
UnreducedLevel{} -> __IMPOSSIBLE__
instance (Subst t a, Normalise a) => Normalise (Abs a) 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 t 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 fs t v as bs) =
ElimCmp cmp fs <$> 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 b cands) = FindInScope m b <$> mapM normalise' cands
normalise' (IsEmpty r t) = IsEmpty r <$> normalise' t
normalise' (CheckSizeLtSat t) = CheckSizeLtSat <$> normalise' t
normalise' c@CheckFunDef{} = return c
normalise' (HasBiggerSort a) = HasBiggerSort <$> normalise' a
normalise' (HasPTSRule a b) = uncurry HasPTSRule <$> normalise' (a,b)
instance Normalise Bool where
normalise' = return
instance Normalise Int where
normalise' = return
instance Normalise Char where
normalise' = return
instance Normalise ConPatternInfo where
normalise' i = normalise' (conPType i) <&> \ t -> i { conPType = t }
instance Normalise DBPatVar where
normalise' = return
instance Normalise a => Normalise (Pattern' a) where
normalise' p = case p of
VarP o x -> VarP o <$> normalise' x
LitP _ -> return p
ConP c mt ps -> ConP c <$> normalise' mt <*> normalise' ps
DotP o v -> DotP o <$> normalise' v
ProjP{} -> return p
instance Normalise DisplayForm where
normalise' (Display n ps v) = Display n <$> normalise' ps <*> return v
instance Normalise e => Normalise (Map k e) where
normalise' = traverse normalise'
instance Normalise a => Normalise (Maybe a) where
normalise' = traverse normalise'
instance Normalise Candidate where
normalise' (Candidate u t eti ov) = Candidate <$> normalise' u <*> normalise' t <*> pure eti <*> pure ov
instance Normalise EqualityView where
normalise' (OtherType t) = OtherType
<$> normalise' t
normalise' (EqualityType s eq l t a b) = EqualityType
<$> normalise' s
<*> return eq
<*> mapM normalise' l
<*> normalise' t
<*> normalise' a
<*> normalise' b
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 -> Type <$> instantiateFull' n
Prop -> return s
PiSort s1 s2 -> piSort <$> instantiateFull' s1 <*> instantiateFull' s2
UnivSort s -> univSort <$> instantiateFull' s
Inf -> return s
SizeUniv -> return s
MetaS x es -> MetaS x <$> instantiateFull' es
instance (InstantiateFull a) => InstantiateFull (Type' a) 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 ci vs -> Con c ci <$> 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 -> Sort <$> instantiateFull' s
Pi a b -> uncurry Pi <$> instantiateFull' (a,b)
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 v of
MetaV m vs -> return $ MetaLevel m vs
_ -> return $ UnreducedLevel v
NeutralLevel r v -> NeutralLevel r <$> instantiateFull' v
BlockedLevel m v ->
ifM (isInstantiatedMeta m)
(UnreducedLevel <$> instantiateFull' v)
(BlockedLevel m <$> instantiateFull' v)
UnreducedLevel v -> UnreducedLevel <$> instantiateFull' v
instance InstantiateFull Substitution where
instantiateFull' sigma =
case sigma of
IdS -> return IdS
EmptyS err -> return $ EmptyS err
Wk n sigma -> Wk n <$> instantiateFull' sigma
Lift n sigma -> Lift n <$> instantiateFull' sigma
Strengthen bot sigma -> Strengthen bot <$> instantiateFull' sigma
t :# sigma -> consS <$> instantiateFull' t
<*> instantiateFull' sigma
instance InstantiateFull Bool where
instantiateFull' = return
instance InstantiateFull Int where
instantiateFull' = return
instance InstantiateFull ConPatternInfo where
instantiateFull' i = instantiateFull' (conPType i) <&> \ t -> i { conPType = t }
instance InstantiateFull DBPatVar where
instantiateFull' = return
instance InstantiateFull a => InstantiateFull (Pattern' a) where
instantiateFull' (VarP o x) = VarP o <$> instantiateFull' x
instantiateFull' (DotP o t) = DotP o <$> instantiateFull' t
instantiateFull' (ConP n mt ps) = ConP n <$> instantiateFull' mt <*> instantiateFull' ps
instantiateFull' l@LitP{} = return l
instantiateFull' p@ProjP{} = return p
instance (Subst t a, InstantiateFull a) => InstantiateFull (Abs a) 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 fs t v as bs ->
ElimCmp cmp fs <$> 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 b cands -> FindInScope m b <$> mapM instantiateFull' cands
IsEmpty r t -> IsEmpty r <$> instantiateFull' t
CheckSizeLtSat t -> CheckSizeLtSat <$> instantiateFull' t
c@CheckFunDef{} -> return c
HasBiggerSort a -> HasBiggerSort <$> instantiateFull' a
HasPTSRule a b -> uncurry HasPTSRule <$> instantiateFull' (a,b)
instance (InstantiateFull a) => InstantiateFull (Elim' a) where
instantiateFull' (Apply v) = Apply <$> instantiateFull' v
instantiateFull' (Proj o f)= pure $ Proj o f
instance InstantiateFull e => InstantiateFull (Map k e) where
instantiateFull' = traverse instantiateFull'
instance 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 c) = uncurry3 Sig <$> instantiateFull' (a, b, c)
instance InstantiateFull Section where
instantiateFull' (Section tel) = Section <$> instantiateFull' tel
instance (Subst t 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 inst copy ma inj d) = do
(t, df, d) <- instantiateFull' (t, df, d)
return $ Defn rel x t pol occ df i c inst copy ma inj d
instance InstantiateFull NLPat where
instantiateFull' (PVar x y) = return $ PVar x y
instantiateFull' (PWild) = return PWild
instantiateFull' (PDef x y) = PDef <$> instantiateFull' x <*> instantiateFull' y
instantiateFull' (PLam x y) = PLam x <$> instantiateFull' y
instantiateFull' (PPi x y) = PPi <$> instantiateFull' x <*> instantiateFull' y
instantiateFull' (PBoundVar x y) = PBoundVar x <$> instantiateFull' y
instantiateFull' (PTerm x) = PTerm <$> instantiateFull' x
instance InstantiateFull NLPType where
instantiateFull' (NLPType l a) = NLPType
<$> instantiateFull' l
<*> instantiateFull' a
instance InstantiateFull RewriteRule where
instantiateFull' (RewriteRule q gamma f ps rhs t) =
RewriteRule q
<$> instantiateFull' gamma
<*> pure f
<*> instantiateFull' ps
<*> 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 ci vs) = DCon c ci <$> instantiateFull' vs
instantiateFull' (DDef c es) = DDef c <$> instantiateFull' es
instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws)
instance InstantiateFull Defn where
instantiateFull' d = case d of
Axiom{} -> return d
AbstractDefn d -> AbstractDefn <$> instantiateFull' 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{ recClause = cl, recTel = tel } -> do
cl <- instantiateFull' cl
tel <- instantiateFull' tel
return $ d { 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 cop cs eta ls m lz) =
Branches cop
<$> instantiateFull' cs
<*> instantiateFull' eta
<*> instantiateFull' ls
<*> instantiateFull' m
<*> pure lz
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 rl rf tel ps b t catchall unreachable) =
Clause rl rf <$> instantiateFull' tel
<*> instantiateFull' ps
<*> instantiateFull' b
<*> instantiateFull' t
<*> return catchall
<*> return unreachable
instance InstantiateFull Interface where
instantiateFull' (Interface h ms mod scope inside
sig display userwarn b foreignCode
highlighting pragmas patsyns warnings) =
Interface h ms mod scope inside
<$> instantiateFull' sig
<*> instantiateFull' display
<*> return userwarn
<*> instantiateFull' b
<*> return foreignCode
<*> return highlighting
<*> return pragmas
<*> return patsyns
<*> return warnings
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 ConHead where
instantiateFull' = return
instance InstantiateFull a => InstantiateFull (Maybe a) where
instantiateFull' = mapM instantiateFull'
instance InstantiateFull Candidate where
instantiateFull' (Candidate u t eti ov) =
Candidate <$> instantiateFull' u <*> instantiateFull' t <*> pure eti <*> pure ov
instance InstantiateFull EqualityView where
instantiateFull' (OtherType t) = OtherType
<$> instantiateFull' t
instantiateFull' (EqualityType s eq l t a b) = EqualityType
<$> instantiateFull' s
<*> return eq
<*> mapM instantiateFull' l
<*> instantiateFull' t
<*> instantiateFull' a
<*> instantiateFull' b