module Agda.Syntax.Abstract
( module Agda.Syntax.Abstract
, module Agda.Syntax.Abstract.Name
) where
import Prelude hiding (foldl, foldr)
import Control.Arrow ((***), first, second)
import Control.Applicative
import Data.Sequence (Seq, (<|), (><))
import qualified Data.Sequence as Seq
import Data.Foldable as Fold
import Data.Traversable
import Data.Map (Map)
import Data.Typeable (Typeable)
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Info
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Abstract.Name as A (QNamed)
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Base
import Agda.Utils.Geniplate
import Agda.Utils.Tuple
#include "../undefined.h"
import Agda.Utils.Impossible
type Color = Expr
type Arg a = Common.Arg Color a
type Dom a = Common.Dom Color a
type NamedArg a = Common.NamedArg Color a
type ArgInfo = Common.ArgInfo Color
type Args = [NamedArg Expr]
instance Eq Color where
Var x == Var y = x == y
Def x == Def y = x == y
_ == _ = __IMPOSSIBLE__
instance Ord Color where
Var x <= Var y = x <= y
Def x <= Def y = x <= y
_ <= _ = __IMPOSSIBLE__
data Expr
= Var Name
| Def QName
| Con AmbiguousQName
| Lit Literal
| QuestionMark MetaInfo InteractionId
| Underscore MetaInfo
| App ExprInfo Expr (NamedArg Expr)
| WithApp ExprInfo Expr [Expr]
| Lam ExprInfo LamBinding Expr
| AbsurdLam ExprInfo Hiding
| ExtendedLam ExprInfo DefInfo QName [Clause]
| Pi ExprInfo Telescope Expr
| Fun ExprInfo (Arg Expr) Expr
| Set ExprInfo Integer
| Prop ExprInfo
| Let ExprInfo [LetBinding] Expr
| ETel Telescope
| Rec ExprInfo Assigns
| RecUpdate ExprInfo Expr Assigns
| ScopedExpr ScopeInfo Expr
| QuoteGoal ExprInfo Name Expr
| QuoteContext ExprInfo Name Expr
| Quote ExprInfo
| QuoteTerm ExprInfo
| Unquote ExprInfo
| DontCare Expr
| PatternSyn QName
deriving (Typeable, Show)
type Assign = (C.Name, Expr)
type Assigns = [Assign]
data Axiom
= FunSig
| NoFunSig
deriving (Typeable, Eq, Ord, Show)
data Declaration
= Axiom Axiom DefInfo ArgInfo QName Expr
| Field DefInfo QName (Arg Expr)
| Primitive DefInfo QName Expr
| Mutual MutualInfo [Declaration]
| Section ModuleInfo ModuleName [TypedBindings] [Declaration]
| Apply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
| Import ModuleInfo ModuleName
| Pragma Range Pragma
| Open ModuleInfo ModuleName
| FunDef DefInfo QName Delayed [Clause]
| DataSig DefInfo QName Telescope Expr
| DataDef DefInfo QName [LamBinding] [Constructor]
| RecSig DefInfo QName Telescope Expr
| RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe QName) [LamBinding] Expr [Declaration]
| PatternSynDef QName [Arg Name] Pattern
| ScopedDecl ScopeInfo [Declaration]
deriving (Typeable, Show)
class GetDefInfo a where
getDefInfo :: a -> Maybe DefInfo
instance GetDefInfo Declaration where
getDefInfo (Axiom _ i _ _ _) = Just i
getDefInfo (Field i _ _) = Just i
getDefInfo (Primitive i _ _) = Just i
getDefInfo (ScopedDecl _ (d:_)) = getDefInfo d
getDefInfo (FunDef i _ _ _) = Just i
getDefInfo (DataSig i _ _ _) = Just i
getDefInfo (DataDef i _ _ _) = Just i
getDefInfo (RecSig i _ _ _) = Just i
getDefInfo (RecDef i _ _ _ _ _ _) = Just i
getDefInfo _ = Nothing
data ModuleApplication
= SectionApp Telescope ModuleName [NamedArg Expr]
| RecordModuleIFS ModuleName
deriving (Typeable, Show)
data Pragma = OptionsPragma [String]
| BuiltinPragma String Expr
| CompiledPragma QName String
| CompiledExportPragma QName String
| CompiledTypePragma QName String
| CompiledDataPragma QName String [String]
| CompiledEpicPragma QName String
| CompiledJSPragma QName String
| StaticPragma QName
| EtaPragma QName
deriving (Typeable, Show)
data LetBinding
= LetBind LetInfo ArgInfo Name Expr Expr
| LetPatBind LetInfo Pattern Expr
| LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
| LetOpen ModuleInfo ModuleName
deriving (Typeable, Show)
type TypeSignature = Declaration
type Constructor = TypeSignature
type Field = TypeSignature
data LamBinding
= DomainFree ArgInfo Name
| DomainFull TypedBindings
deriving (Typeable, Show)
data TypedBindings = TypedBindings Range (Arg TypedBinding)
deriving (Typeable, Show)
data TypedBinding
= TBind Range [Name] Expr
| TLet Range [LetBinding]
deriving (Typeable, Show)
type Telescope = [TypedBindings]
data Clause' lhs = Clause
{ clauseLHS :: lhs
, clauseRHS :: RHS
, clauseWhereDecls :: [Declaration]
} deriving (Typeable, Show, Functor, Foldable, Traversable)
type Clause = Clause' LHS
type SpineClause = Clause' SpineLHS
data RHS = RHS Expr
| AbsurdRHS
| WithRHS QName [Expr] [Clause]
| RewriteRHS [QName] [Expr] RHS [Declaration]
deriving (Typeable, Show)
data SpineLHS = SpineLHS
{ spLhsInfo :: LHSInfo
, spLhsDefName :: QName
, spLhsPats :: [NamedArg Pattern]
, spLhsWithPats :: [Pattern]
}
deriving (Typeable, Show)
data LHS = LHS
{ lhsInfo :: LHSInfo
, lhsCore :: LHSCore
, lhsWithPats :: [Pattern]
}
deriving (Typeable, Show)
data LHSCore' e
= LHSHead { lhsDefName :: QName
, lhsPats :: [NamedArg (Pattern' e)]
}
| LHSProj { lhsDestructor :: QName
, lhsPatsLeft :: [NamedArg (Pattern' e)]
, lhsFocus :: NamedArg (LHSCore' e)
, lhsPatsRight :: [NamedArg (Pattern' e)]
}
deriving (Typeable, Show, Functor, Foldable, Traversable)
type LHSCore = LHSCore' Expr
class LHSToSpine a b where
lhsToSpine :: a -> b
spineToLhs :: b -> a
instance LHSToSpine LHS SpineLHS where
lhsToSpine (LHS i core wps) = SpineLHS i f ps wps
where QNamed f ps = lhsCoreToSpine core
spineToLhs (SpineLHS i f ps wps) = LHS i (spineToLhsCore $ QNamed f ps) wps
instance LHSToSpine Clause SpineClause where
lhsToSpine = fmap lhsToSpine
spineToLhs = fmap spineToLhs
instance LHSToSpine a b => LHSToSpine [a] [b] where
lhsToSpine = map lhsToSpine
spineToLhs = map spineToLhs
lhsCoreToSpine :: LHSCore' e -> A.QNamed [NamedArg (Pattern' e)]
lhsCoreToSpine (LHSHead f ps) = QNamed f ps
lhsCoreToSpine (LHSProj d ps1 h ps2) = (++ (p : ps2)) <$> lhsCoreToSpine (namedArg h)
where p = updateNamedArg (const $ DefP patNoRange d ps1) h
spineToLhsCore :: QNamed [NamedArg (Pattern' e)] -> LHSCore' e
spineToLhsCore (QNamed f ps) = lhsCoreAddSpine (LHSHead f []) ps
lhsCoreApp :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreApp (LHSHead f ps) ps' = LHSHead f $ ps ++ ps'
lhsCoreApp (LHSProj d ps1 h ps2) ps' = LHSProj d ps1 h $ ps2 ++ ps'
lhsCoreAddSpine :: LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e
lhsCoreAddSpine core ps = case ps2 of
[] -> lhsCoreApp core ps
(Common.Arg info (Named n (DefP i d ps0)) : ps2') ->
LHSProj d ps0 (Common.Arg info $ Named n $ lhsCoreApp core ps1) []
`lhsCoreAddSpine` ps2'
_ -> __IMPOSSIBLE__
where
(ps1, ps2) = break (isDefP . namedArg) ps
isDefP DefP{} = True
isDefP _ = False
lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
lhsCoreAllPatterns = map namedArg . qnamed . lhsCoreToSpine
lhsCoreToPattern :: LHSCore -> Pattern
lhsCoreToPattern lc =
case lc of
LHSHead f aps -> DefP noInfo f aps
LHSProj d aps1 lhscore aps2 -> DefP noInfo d $
aps1 ++ fmap (fmap lhsCoreToPattern) lhscore : aps2
where noInfo = patNoRange
mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
mapLHSHead f (LHSHead x ps) = f x ps
mapLHSHead f (LHSProj d ps1 l ps2) =
LHSProj d ps1 (fmap (fmap (mapLHSHead f)) l) ps2
data Pattern' e
= VarP Name
| ConP ConPatInfo AmbiguousQName [NamedArg (Pattern' e)]
| DefP PatInfo QName [NamedArg (Pattern' e)]
| WildP PatInfo
| AsP PatInfo Name (Pattern' e)
| DotP PatInfo e
| AbsurdP PatInfo
| LitP Literal
| ImplicitP PatInfo
| PatternSynP PatInfo QName [NamedArg (Pattern' e)]
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Pattern = Pattern' Expr
type Patterns = [NamedArg Pattern]
class IsProjP a where
isProjP :: a -> Maybe QName
instance IsProjP (Pattern' e) where
isProjP (DefP _ d []) = Just d
isProjP _ = Nothing
instance IsProjP a => IsProjP (Common.Arg c a) where
isProjP = isProjP . unArg
instance IsProjP a => IsProjP (Named n a) where
isProjP = isProjP . namedThing
instance HasRange LamBinding where
getRange (DomainFree _ x) = getRange x
getRange (DomainFull b) = getRange b
instance HasRange TypedBindings where
getRange (TypedBindings r _) = r
instance HasRange TypedBinding where
getRange (TBind r _ _) = r
getRange (TLet r _) = r
instance HasRange Expr where
getRange (Var x) = getRange x
getRange (Def x) = getRange x
getRange (Con x) = getRange x
getRange (Lit l) = getRange l
getRange (QuestionMark i _) = getRange i
getRange (Underscore i) = getRange i
getRange (App i _ _) = getRange i
getRange (WithApp i _ _) = getRange i
getRange (Lam i _ _) = getRange i
getRange (AbsurdLam i _) = getRange i
getRange (ExtendedLam i _ _ _) = getRange i
getRange (Pi i _ _) = getRange i
getRange (Fun i _ _) = getRange i
getRange (Set i _) = getRange i
getRange (Prop i) = getRange i
getRange (Let i _ _) = getRange i
getRange (Rec i _) = getRange i
getRange (RecUpdate i _ _) = getRange i
getRange (ETel tel) = getRange tel
getRange (ScopedExpr _ e) = getRange e
getRange (QuoteGoal _ _ e) = getRange e
getRange (QuoteContext _ _ e) = getRange e
getRange (Quote i) = getRange i
getRange (QuoteTerm i) = getRange i
getRange (Unquote i) = getRange i
getRange (DontCare{}) = noRange
getRange (PatternSyn x) = getRange x
instance HasRange Declaration where
getRange (Axiom _ i _ _ _ ) = getRange i
getRange (Field i _ _ ) = getRange i
getRange (Mutual i _ ) = getRange i
getRange (Section i _ _ _ ) = getRange i
getRange (Apply i _ _ _ _ ) = getRange i
getRange (Import i _ ) = getRange i
getRange (Primitive i _ _ ) = getRange i
getRange (Pragma i _ ) = getRange i
getRange (Open i _ ) = getRange i
getRange (ScopedDecl _ d ) = getRange d
getRange (FunDef i _ _ _ ) = getRange i
getRange (DataSig i _ _ _ ) = getRange i
getRange (DataDef i _ _ _ ) = getRange i
getRange (RecSig i _ _ _ ) = getRange i
getRange (RecDef i _ _ _ _ _ _) = getRange i
getRange (PatternSynDef x _ _ ) = getRange x
instance HasRange (Pattern' e) where
getRange (VarP x) = getRange x
getRange (ConP i _ _) = getRange i
getRange (DefP i _ _) = getRange i
getRange (WildP i) = getRange i
getRange (ImplicitP i) = getRange i
getRange (AsP i _ _) = getRange i
getRange (DotP i _) = getRange i
getRange (AbsurdP i) = getRange i
getRange (LitP l) = getRange l
getRange (PatternSynP i _ _) = getRange i
instance HasRange SpineLHS where
getRange (SpineLHS i _ _ _) = getRange i
instance HasRange LHS where
getRange (LHS i _ _) = getRange i
instance HasRange (LHSCore' e) where
getRange (LHSHead f ps) = fuseRange f ps
getRange (LHSProj d ps1 lhscore ps2) = d `fuseRange` ps1 `fuseRange` lhscore `fuseRange` ps2
instance HasRange a => HasRange (Clause' a) where
getRange (Clause lhs rhs ds) = getRange (lhs,rhs,ds)
instance HasRange RHS where
getRange AbsurdRHS = noRange
getRange (RHS e) = getRange e
getRange (WithRHS _ e cs) = fuseRange e cs
getRange (RewriteRHS _ es rhs wh) = getRange (es, rhs, wh)
instance HasRange LetBinding where
getRange (LetBind i _ _ _ _ ) = getRange i
getRange (LetPatBind i _ _ ) = getRange i
getRange (LetApply i _ _ _ _ ) = getRange i
getRange (LetOpen i _ ) = getRange i
instance SetRange (Pattern' a) where
setRange r (VarP x) = VarP (setRange r x)
setRange r (ConP i ns as) = ConP (setRange r i) ns as
setRange r (DefP _ n as) = DefP (PatRange r) (setRange r n) as
setRange r (WildP _) = WildP (PatRange r)
setRange r (ImplicitP _) = ImplicitP (PatRange r)
setRange r (AsP _ n p) = AsP (PatRange r) (setRange r n) p
setRange r (DotP _ e) = DotP (PatRange r) e
setRange r (AbsurdP _) = AbsurdP (PatRange r)
setRange r (LitP l) = LitP (setRange r l)
setRange r (PatternSynP _ n as) = PatternSynP (PatRange r) (setRange r n) as
instance KillRange LamBinding where
killRange (DomainFree info x) = killRange1 (DomainFree info) x
killRange (DomainFull b) = killRange1 DomainFull b
instance KillRange TypedBindings where
killRange (TypedBindings r b) = TypedBindings (killRange r) (killRange b)
instance KillRange TypedBinding where
killRange (TBind r xs e) = killRange3 TBind r xs e
killRange (TLet r lbs) = killRange2 TLet r lbs
instance KillRange Expr where
killRange (Var x) = killRange1 Var x
killRange (Def x) = killRange1 Def x
killRange (Con x) = killRange1 Con x
killRange (Lit l) = killRange1 Lit l
killRange (QuestionMark i ii) = killRange2 QuestionMark i ii
killRange (Underscore i) = killRange1 Underscore i
killRange (App i e1 e2) = killRange3 App i e1 e2
killRange (WithApp i e es) = killRange3 WithApp i e es
killRange (Lam i b e) = killRange3 Lam i b e
killRange (AbsurdLam i h) = killRange1 AbsurdLam i h
killRange (ExtendedLam i n d ps) = killRange4 ExtendedLam i n d ps
killRange (Pi i a b) = killRange3 Pi i a b
killRange (Fun i a b) = killRange3 Fun i a b
killRange (Set i n) = Set (killRange i) n
killRange (Prop i) = killRange1 Prop i
killRange (Let i ds e) = killRange3 Let i ds e
killRange (Rec i fs) = Rec (killRange i) (map (id -*- killRange) fs)
killRange (RecUpdate i e fs) = RecUpdate (killRange i)
(killRange e)
(map (id -*- killRange) fs)
killRange (ETel tel) = killRange1 ETel tel
killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e
killRange (QuoteGoal i x e) = killRange3 QuoteGoal i x e
killRange (QuoteContext i x e) = killRange3 QuoteContext i x e
killRange (Quote i) = killRange1 Quote i
killRange (QuoteTerm i) = killRange1 QuoteTerm i
killRange (Unquote i) = killRange1 Unquote i
killRange (DontCare e) = DontCare e
killRange (PatternSyn x) = killRange1 PatternSyn x
instance KillRange Declaration where
killRange (Axiom p i rel a b ) = killRange4 (Axiom p) i rel a b
killRange (Field i a b ) = killRange3 Field i a b
killRange (Mutual i a ) = killRange2 Mutual i a
killRange (Section i a b c ) = killRange4 Section i a b c
killRange (Apply i a b c d ) = killRange3 Apply i a b c d
killRange (Import i a ) = killRange2 Import i a
killRange (Primitive i a b ) = killRange3 Primitive i a b
killRange (Pragma i a ) = Pragma (killRange i) a
killRange (Open i x ) = killRange2 Open i x
killRange (ScopedDecl a d ) = killRange1 (ScopedDecl a) d
killRange (FunDef i a b c ) = killRange4 FunDef i a b c
killRange (DataSig i a b c ) = killRange4 DataSig i a b c
killRange (DataDef i a b c ) = killRange4 DataDef i a b c
killRange (RecSig i a b c ) = killRange4 RecSig i a b c
killRange (RecDef i a b c d e f ) = killRange7 RecDef i a b c d e f
killRange (PatternSynDef x xs p ) = killRange3 PatternSynDef x xs p
instance KillRange ModuleApplication where
killRange (SectionApp a b c ) = killRange3 SectionApp a b c
killRange (RecordModuleIFS a ) = killRange1 RecordModuleIFS a
instance KillRange x => KillRange (ThingWithFixity x) where
killRange (ThingWithFixity c f) = ThingWithFixity (killRange c) f
instance KillRange e => KillRange (Pattern' e) where
killRange (VarP x) = killRange1 VarP x
killRange (ConP i a b) = killRange3 ConP i a b
killRange (DefP i a b) = killRange3 DefP i a b
killRange (WildP i) = killRange1 WildP i
killRange (ImplicitP i) = killRange1 ImplicitP i
killRange (AsP i a b) = killRange3 AsP i a b
killRange (DotP i a) = killRange2 DotP i a
killRange (AbsurdP i) = killRange1 AbsurdP i
killRange (LitP l) = killRange1 LitP l
killRange (PatternSynP i a p) = killRange3 PatternSynP i a p
instance KillRange SpineLHS where
killRange (SpineLHS i a b c) = killRange4 SpineLHS i a b c
instance KillRange LHS where
killRange (LHS i a b) = killRange3 LHS i a b
instance KillRange e => KillRange (LHSCore' e) where
killRange (LHSHead a b) = killRange2 LHSHead a b
killRange (LHSProj a b c d) = killRange4 LHSProj a b c d
instance KillRange a => KillRange (Clause' a) where
killRange (Clause lhs rhs ds) = killRange3 Clause lhs rhs ds
instance KillRange RHS where
killRange AbsurdRHS = AbsurdRHS
killRange (RHS e) = killRange1 RHS e
killRange (WithRHS q e cs) = killRange3 WithRHS q e cs
killRange (RewriteRHS x es rhs wh) = killRange4 RewriteRHS x es rhs wh
instance KillRange LetBinding where
killRange (LetBind i info a b c) = killRange5 LetBind i info a b c
killRange (LetPatBind i a b ) = killRange3 LetPatBind i a b
killRange (LetApply i a b c d ) = killRange3 LetApply i a b c d
killRange (LetOpen i x ) = killRange2 LetOpen i x
instanceUniverseBiT' [] [t| (Declaration, QName) |]
instanceUniverseBiT' [] [t| (Declaration, AmbiguousQName) |]
instanceUniverseBiT' [] [t| (Declaration, Expr) |]
instanceUniverseBiT' [] [t| (Declaration, LetBinding) |]
instanceUniverseBiT' [] [t| (Declaration, LamBinding) |]
instanceUniverseBiT' [] [t| (Declaration, TypedBinding) |]
instanceUniverseBiT' [] [t| (Declaration, Pattern) |]
instanceUniverseBiT' [] [t| (Declaration, Declaration) |]
instanceUniverseBiT' [] [t| (Declaration, ModuleName) |]
instanceUniverseBiT' [] [t| (Declaration, ModuleInfo) |]
instanceUniverseBiT' [] [t| (Declaration, RString) |]
allNames :: Declaration -> Seq QName
allNames (Axiom _ _ _ q _) = Seq.singleton q
allNames (Field _ q _) = Seq.singleton q
allNames (Primitive _ q _) = Seq.singleton q
allNames (Mutual _ defs) = Fold.foldMap allNames defs
allNames (DataSig _ q _ _) = Seq.singleton q
allNames (DataDef _ q _ decls) = q <| Fold.foldMap allNames decls
allNames (RecSig _ q _ _) = Seq.singleton q
allNames (RecDef _ q _ c _ _ decls) =
q <| foldMap Seq.singleton c >< Fold.foldMap allNames decls
allNames (PatternSynDef q _ _) = Seq.singleton q
allNames (FunDef _ q _ cls) = q <| Fold.foldMap allNamesC cls
where
allNamesC :: Clause -> Seq QName
allNamesC (Clause _ rhs decls) = allNamesR rhs ><
Fold.foldMap allNames decls
allNamesR :: RHS -> Seq QName
allNamesR (RHS e) = allNamesE e
allNamesR AbsurdRHS {} = Seq.empty
allNamesR (WithRHS q _ cls) = q <| Fold.foldMap allNamesC cls
allNamesR (RewriteRHS qs _ rhs cls) =
Seq.fromList qs >< allNamesR rhs
>< Fold.foldMap allNames cls
allNamesE :: Expr -> Seq QName
allNamesE Var {} = Seq.empty
allNamesE Def {} = Seq.empty
allNamesE Con {} = Seq.empty
allNamesE Lit {} = Seq.empty
allNamesE QuestionMark {} = Seq.empty
allNamesE Underscore {} = Seq.empty
allNamesE (App _ e1 e2) = Fold.foldMap allNamesE [e1, namedThing (unArg e2)]
allNamesE (WithApp _ e es) = Fold.foldMap allNamesE (e : es)
allNamesE (Lam _ b e) = allNamesLam b >< allNamesE e
allNamesE AbsurdLam {} = Seq.empty
allNamesE (ExtendedLam _ _ q cls) = q <| Fold.foldMap allNamesC cls
allNamesE (Pi _ tel e) = Fold.foldMap allNamesBinds tel ><
allNamesE e
allNamesE (Fun _ (Common.Arg _ e1) e2) = Fold.foldMap allNamesE [e1, e2]
allNamesE Set {} = Seq.empty
allNamesE Prop {} = Seq.empty
allNamesE (Let _ lbs e) = Fold.foldMap allNamesLet lbs ><
allNamesE e
allNamesE ETel {} = __IMPOSSIBLE__
allNamesE (Rec _ fields) = Fold.foldMap allNamesE (map snd fields)
allNamesE (RecUpdate _ e fs) = allNamesE e >< Fold.foldMap allNamesE (map snd fs)
allNamesE (ScopedExpr _ e) = allNamesE e
allNamesE (QuoteGoal _ _ e) = allNamesE e
allNamesE (QuoteContext _ _ e) = allNamesE e
allNamesE Quote {} = Seq.empty
allNamesE QuoteTerm {} = Seq.empty
allNamesE Unquote {} = Seq.empty
allNamesE DontCare {} = Seq.empty
allNamesE (PatternSyn x) = Seq.empty
allNamesLam :: LamBinding -> Seq QName
allNamesLam DomainFree {} = Seq.empty
allNamesLam (DomainFull binds) = allNamesBinds binds
allNamesBinds :: TypedBindings -> Seq QName
allNamesBinds (TypedBindings _ (Common.Arg _ (TBind _ _ e))) = allNamesE e
allNamesBinds (TypedBindings _ (Common.Arg _ (TLet _ lbs))) = allNamesLets lbs
allNamesLets :: [LetBinding] -> Seq QName
allNamesLets = Fold.foldMap allNamesLet
allNamesLet :: LetBinding -> Seq QName
allNamesLet (LetBind _ _ _ e1 e2) = Fold.foldMap allNamesE [e1, e2]
allNamesLet (LetPatBind _ _ e) = allNamesE e
allNamesLet (LetApply _ _ app _ _) = allNamesApp app
allNamesLet LetOpen {} = Seq.empty
allNamesApp :: ModuleApplication -> Seq QName
allNamesApp (SectionApp bindss _ es) = Fold.foldMap allNamesBinds bindss ><
Fold.foldMap allNamesE (map namedArg es)
allNamesApp RecordModuleIFS {} = Seq.empty
allNames (Section _ _ _ decls) = Fold.foldMap allNames decls
allNames Apply {} = Seq.empty
allNames Import {} = Seq.empty
allNames Pragma {} = Seq.empty
allNames Open {} = Seq.empty
allNames (ScopedDecl _ decls) = Fold.foldMap allNames decls
axiomName :: Declaration -> QName
axiomName (Axiom _ _ _ q _) = q
axiomName (ScopedDecl _ (d:_)) = axiomName d
axiomName _ = __IMPOSSIBLE__
class AnyAbstract a where
anyAbstract :: a -> Bool
instance AnyAbstract a => AnyAbstract [a] where
anyAbstract = Fold.any anyAbstract
instance AnyAbstract Declaration where
anyAbstract (Axiom _ i _ _ _) = defAbstract i == AbstractDef
anyAbstract (Field i _ _) = defAbstract i == AbstractDef
anyAbstract (Mutual _ ds) = anyAbstract ds
anyAbstract (ScopedDecl _ ds) = anyAbstract ds
anyAbstract (Section _ _ _ ds) = anyAbstract ds
anyAbstract (FunDef i _ _ _) = defAbstract i == AbstractDef
anyAbstract (DataDef i _ _ _) = defAbstract i == AbstractDef
anyAbstract (RecDef i _ _ _ _ _ _) = defAbstract i == AbstractDef
anyAbstract (DataSig i _ _ _) = defAbstract i == AbstractDef
anyAbstract (RecSig i _ _ _) = defAbstract i == AbstractDef
anyAbstract _ = __IMPOSSIBLE__
app = foldl (App (ExprRange noRange))
patternToExpr :: Pattern -> Expr
patternToExpr (VarP x) = Var x
patternToExpr (ConP _ c ps) =
Con c `app` map (fmap (fmap patternToExpr)) ps
patternToExpr (DefP _ f ps) =
Def f `app` map (fmap (fmap patternToExpr)) ps
patternToExpr (WildP _) = Underscore emptyMetaInfo
patternToExpr (AsP _ _ p) = patternToExpr p
patternToExpr (DotP _ e) = e
patternToExpr (AbsurdP _) = Underscore emptyMetaInfo
patternToExpr (LitP l) = Lit l
patternToExpr (ImplicitP _) = Underscore emptyMetaInfo
patternToExpr (PatternSynP _ _ _) = __IMPOSSIBLE__
type PatternSynDefn = ([Arg Name], Pattern)
type PatternSynDefns = Map QName PatternSynDefn
lambdaLiftExpr :: [Name] -> Expr -> Expr
lambdaLiftExpr [] e = e
lambdaLiftExpr (n:ns) e = Lam (ExprRange noRange)
(DomainFree defaultArgInfo n) $
lambdaLiftExpr ns e
substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
substPattern s p = case p of
VarP z -> case lookup z s of
Nothing -> p
Just x -> x
ConP i q ps -> ConP i q (fmap (fmap (fmap (substPattern s))) ps)
WildP i -> p
DotP i e -> DotP i (substExpr (map (fmap patternToExpr) s) e)
AbsurdP i -> p
LitP l -> p
_ -> __IMPOSSIBLE__
substExpr :: [(Name, Expr)] -> Expr -> Expr
substExpr s e = case e of
Var n -> case lookup n s of
Nothing -> e
Just z -> z
Def _ -> e
Con _ -> e
Lit _ -> e
QuestionMark{} -> e
Underscore _ -> e
App i e e' -> App i (substExpr s e)
(fmap (fmap (substExpr s)) e')
WithApp i e es -> WithApp i (substExpr s e)
(fmap (substExpr s) es)
Lam i lb e -> Lam i lb (substExpr s e)
AbsurdLam i h -> e
ExtendedLam i di n cs -> __IMPOSSIBLE__
Pi i t e -> Pi i (fmap (substTypedBindings s) t)
(substExpr s e)
Fun i ae e -> Fun i (fmap (substExpr s) ae)
(substExpr s e)
Set i n -> e
Prop i -> e
Let i ls e -> Let i (substLetBindings s ls)
(substExpr s e)
ETel t -> e
Rec i nes -> Rec i (fmap (fmap (substExpr s)) nes)
RecUpdate i e nes -> RecUpdate i (substExpr s e)
(fmap (fmap (substExpr s)) nes)
ScopedExpr si e -> ScopedExpr si (substExpr s e)
QuoteGoal i n e -> QuoteGoal i n (substExpr s e)
QuoteContext i n e -> QuoteContext i n (substExpr s e)
Quote i -> e
QuoteTerm i -> e
Unquote i -> e
DontCare e -> DontCare (substExpr s e)
PatternSyn x -> e
substLetBindings :: [(Name, Expr)] -> [LetBinding] -> [LetBinding]
substLetBindings s = fmap (substLetBinding s)
substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBinding
substLetBinding s lb = case lb of
LetBind i r n e e' -> LetBind i r n (substExpr s e) (substExpr s e')
LetPatBind i p e -> LetPatBind i p (substExpr s e)
_ -> lb
substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindings
substTypedBindings s (TypedBindings r atb) = TypedBindings r
(fmap (substTypedBinding s) atb)
substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBinding
substTypedBinding s tb = case tb of
TBind r ns e -> TBind r ns $ substExpr s e
TLet r lbs -> TLet r $ substLetBindings s lbs
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] ->
Maybe ([(Name, a)], [Arg Name])
insertImplicitPatSynArgs wild r ns as = matchArgs r ns as
where
matchNextArg r n as@(~(a : as'))
| matchNext n as = return (namedArg a, as')
| getHiding n == NotHidden = Nothing
| otherwise = return (wild r, as)
matchNext _ [] = False
matchNext n (a:as) = getHiding n == getHiding a && matchName
where
x = unranged $ show $ nameConcrete $ unArg n
matchName = maybe True (== x) (nameOf $ unArg a)
matchArgs r [] [] = return ([], [])
matchArgs r [] as = Nothing
matchArgs r (n:ns) [] | getHiding n == NotHidden = return ([], n : ns)
matchArgs r (n:ns) as = do
(p, as) <- matchNextArg r n as
first ((unArg n, p) :) <$> matchArgs (getRange p) ns as