{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Abstract
( module Agda.Syntax.Abstract
, module Agda.Syntax.Abstract.Name
) where
import Prelude
import Control.Arrow (first)
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Function (on)
import Data.Map (Map)
import Data.Maybe
import Data.Sequence (Seq, (<|), (><))
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Void
import Data.Data (Data)
import Data.Monoid (mappend)
import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Abstract.Name as A (QNamed)
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.Geniplate
import Agda.Utils.Lens
import Agda.Utils.Pretty
import Agda.Utils.Impossible
newtype BindName = BindName { unBind :: Name }
deriving (Show, Data, HasRange, KillRange, SetRange)
mkBindName :: Name -> BindName
mkBindName x = BindName x
instance Eq BindName where
BindName n == BindName m
= ((==) `on` nameId) n m
&& ((==) `on` nameConcrete) n m
instance Ord BindName where
BindName n `compare` BindName m
= (compare `on` nameId) n m
`mappend` (compare `on` nameConcrete) n m
type Args = [NamedArg Expr]
data Expr
= Var Name
| Def QName
| Proj ProjOrigin AmbiguousQName
| Con AmbiguousQName
| PatternSyn AmbiguousQName
| Macro QName
| Lit Literal
| QuestionMark MetaInfo InteractionId
| Underscore MetaInfo
| Dot ExprInfo Expr
| App AppInfo Expr (NamedArg Expr)
| WithApp ExprInfo Expr [Expr]
| Lam ExprInfo LamBinding Expr
| AbsurdLam ExprInfo Hiding
| ExtendedLam ExprInfo DefInfo QName [Clause]
| Pi ExprInfo Telescope Expr
| Generalized (Set.Set QName) Expr
| Fun ExprInfo (Arg Expr) Expr
| Set ExprInfo Integer
| Prop ExprInfo Integer
| Let ExprInfo [LetBinding] Expr
| ETel Telescope
| Rec ExprInfo RecordAssigns
| RecUpdate ExprInfo Expr Assigns
| ScopedExpr ScopeInfo Expr
| Quote ExprInfo
| QuoteTerm ExprInfo
| Unquote ExprInfo
| Tactic ExprInfo Expr [NamedArg Expr]
| DontCare Expr
deriving (Data, Show)
generalized :: Set.Set QName -> Expr -> Expr
generalized s e
| Set.null s = e
| otherwise = Generalized s e
type Assign = FieldAssignment' Expr
type Assigns = [Assign]
type RecordAssign = Either Assign ModuleName
type RecordAssigns = [RecordAssign]
data Axiom
= FunSig
| NoFunSig
deriving (Data, Eq, Ord, Show)
type Ren a = [(a, a)]
data ScopeCopyInfo = ScopeCopyInfo
{ renModules :: Ren ModuleName
, renNames :: Ren QName }
deriving (Eq, Show, Data)
initCopyInfo :: ScopeCopyInfo
initCopyInfo = ScopeCopyInfo
{ renModules = []
, renNames = []
}
instance Pretty ScopeCopyInfo where
pretty i = vcat [ prRen "renModules =" (renModules i)
, prRen "renNames =" (renNames i) ]
where
prRen s r = sep [ text s, nest 2 $ vcat (map pr r) ]
pr (x, y) = pretty x <+> "->" <+> pretty y
data Declaration
= Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr
| Generalize (Set.Set QName) DefInfo ArgInfo QName Expr
| Field DefInfo QName (Arg Expr)
| Primitive DefInfo QName Expr
| Mutual MutualInfo [Declaration]
| Section ModuleInfo ModuleName GeneralizeTelescope [Declaration]
| Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
| Import ModuleInfo ModuleName ImportDirective
| Pragma Range Pragma
| Open ModuleInfo ModuleName ImportDirective
| FunDef DefInfo QName Delayed [Clause]
| DataSig DefInfo QName GeneralizeTelescope Expr
| DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
| RecSig DefInfo QName GeneralizeTelescope Expr
| RecDef DefInfo QName UniverseCheck (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) DataDefParams Expr [Declaration]
| PatternSynDef QName [Arg Name] (Pattern' Void)
| UnquoteDecl MutualInfo [DefInfo] [QName] Expr
| UnquoteDef [DefInfo] [QName] Expr
| ScopedDecl ScopeInfo [Declaration]
deriving (Data, Show)
type DefInfo = DefInfo' Expr
type ImportDirective = ImportDirective' QName ModuleName
type Renaming = Renaming' QName ModuleName
type ImportedName = ImportedName' QName ModuleName
data ModuleApplication
= SectionApp Telescope ModuleName [NamedArg Expr]
| RecordModuleInstance ModuleName
deriving (Data, Show, Eq)
data Pragma
= OptionsPragma [String]
| BuiltinPragma RString ResolvedName
| BuiltinNoDefPragma RString QName
| RewritePragma Range [QName]
| CompilePragma RString QName String
| StaticPragma QName
| EtaPragma QName
| InjectivePragma QName
| InlinePragma Bool QName
| DisplayPragma QName [NamedArg Pattern] Expr
deriving (Data, Show, Eq)
data LetBinding
= LetBind LetInfo ArgInfo BindName Expr Expr
| LetPatBind LetInfo Pattern Expr
| LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
| LetOpen ModuleInfo ModuleName ImportDirective
| LetDeclaredVariable BindName
deriving (Data, Show, Eq)
type TypeSignature = Declaration
type Constructor = TypeSignature
type Field = TypeSignature
type TacticAttr = Maybe Expr
data Binder' a = Binder
{ binderPattern :: Maybe Pattern
, binderName :: a
} deriving (Data, Show, Eq, Functor, Foldable, Traversable)
type Binder = Binder' BindName
mkBinder :: a -> Binder' a
mkBinder = Binder Nothing
mkBinder_ :: Name -> Binder
mkBinder_ = mkBinder . mkBindName
extractPattern :: Binder' a -> Maybe (Pattern, a)
extractPattern (Binder p a) = (,a) <$> p
data LamBinding
= DomainFree TacticAttr (NamedArg Binder)
| DomainFull TypedBinding
deriving (Data, Show, Eq)
mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree = DomainFree Nothing
data TypedBinding
= TBind Range TacticAttr [NamedArg Binder] Expr
| TLet Range [LetBinding]
deriving (Data, Show, Eq)
mkTBind :: Range -> [NamedArg Binder] -> Expr -> TypedBinding
mkTBind r = TBind r Nothing
type Telescope = [TypedBinding]
data GeneralizeTelescope = GeneralizeTel
{ generalizeTelVars :: Map QName Name
, generalizeTel :: Telescope }
deriving (Data, Show, Eq)
data DataDefParams = DataDefParams
{ dataDefGeneralizedParams :: Set Name
, dataDefParams :: [LamBinding]
}
deriving (Data, Show, Eq)
noDataDefParams :: DataDefParams
noDataDefParams = DataDefParams Set.empty []
data ProblemEq = ProblemEq
{ problemInPat :: Pattern
, problemInst :: I.Term
, problemType :: I.Dom I.Type
} deriving (Data, Show)
instance Eq ProblemEq where _ == _ = True
data Clause' lhs = Clause
{ clauseLHS :: lhs
, clauseStrippedPats :: [ProblemEq]
, clauseRHS :: RHS
, clauseWhereDecls :: WhereDeclarations
, clauseCatchall :: Bool
} deriving (Data, Show, Functor, Foldable, Traversable, Eq)
data WhereDeclarations = WhereDecls
{ whereModule :: Maybe ModuleName
, whereDecls :: [Declaration]
} deriving (Data, Show, Eq)
noWhereDecls :: WhereDeclarations
noWhereDecls = WhereDecls Nothing []
type Clause = Clause' LHS
type SpineClause = Clause' SpineLHS
type RewriteEqn = RewriteEqn' QName Pattern Expr
data RHS
= RHS
{ rhsExpr :: Expr
, rhsConcrete :: Maybe C.Expr
}
| AbsurdRHS
| WithRHS QName [WithHiding Expr] [Clause]
| RewriteRHS
{ rewriteExprs :: [RewriteEqn]
, rewriteStrippedPats :: [ProblemEq]
, rewriteRHS :: RHS
, rewriteWhereDecls :: WhereDeclarations
}
deriving (Data, Show)
instance Eq RHS where
RHS e _ == RHS e' _ = e == e'
AbsurdRHS == AbsurdRHS = True
WithRHS a b c == WithRHS a' b' c' = and [ a == a', b == b', c == c' ]
RewriteRHS a b c d == RewriteRHS a' b' c' d' = and [ a == a', b == b', c == c' , d == d' ]
_ == _ = False
data SpineLHS = SpineLHS
{ spLhsInfo :: LHSInfo
, spLhsDefName :: QName
, spLhsPats :: [NamedArg Pattern]
}
deriving (Data, Show, Eq)
instance Eq LHS where
LHS _ core == LHS _ core' = core == core'
data LHS = LHS
{ lhsInfo :: LHSInfo
, lhsCore :: LHSCore
}
deriving (Data, Show)
data LHSCore' e
= LHSHead { lhsDefName :: QName
, lhsPats :: [NamedArg (Pattern' e)]
}
| LHSProj { lhsDestructor :: AmbiguousQName
, lhsFocus :: NamedArg (LHSCore' e)
, lhsPats :: [NamedArg (Pattern' e)]
}
| LHSWith { lhsHead :: LHSCore' e
, lhsWithPatterns :: [Pattern' e]
, lhsPats :: [NamedArg (Pattern' e)]
}
deriving (Data, Show, Functor, Foldable, Traversable, Eq)
type LHSCore = LHSCore' Expr
data Pattern' e
= VarP BindName
| ConP ConPatInfo AmbiguousQName (NAPs e)
| ProjP PatInfo ProjOrigin AmbiguousQName
| DefP PatInfo AmbiguousQName (NAPs e)
| WildP PatInfo
| AsP PatInfo BindName (Pattern' e)
| DotP PatInfo e
| AbsurdP PatInfo
| LitP Literal
| PatternSynP PatInfo AmbiguousQName (NAPs e)
| RecP PatInfo [FieldAssignment' (Pattern' e)]
| EqualP PatInfo [(e, e)]
| WithP PatInfo (Pattern' e)
deriving (Data, Show, Functor, Foldable, Traversable, Eq)
type NAPs e = [NamedArg (Pattern' e)]
type Pattern = Pattern' Expr
type Patterns = [NamedArg Pattern]
instance IsProjP (Pattern' e) where
isProjP (ProjP _ o d) = Just (o, d)
isProjP _ = Nothing
instance IsProjP Expr where
isProjP (Proj o ds) = Just (o, ds)
isProjP (ScopedExpr _ e) = isProjP e
isProjP _ = Nothing
type HoleContent = C.HoleContent' () Pattern Expr
instance Eq Expr where
ScopedExpr _ a1 == ScopedExpr _ a2 = a1 == a2
Var a1 == Var a2 = a1 == a2
Def a1 == Def a2 = a1 == a2
Proj _ a1 == Proj _ a2 = a1 == a2
Con a1 == Con a2 = a1 == a2
PatternSyn a1 == PatternSyn a2 = a1 == a2
Macro a1 == Macro a2 = a1 == a2
Lit a1 == Lit a2 = a1 == a2
QuestionMark a1 b1 == QuestionMark a2 b2 = (a1, b1) == (a2, b2)
Underscore a1 == Underscore a2 = a1 == a2
Dot r1 e1 == Dot r2 e2 = (r1, e1) == (r2, e2)
App a1 b1 c1 == App a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
WithApp a1 b1 c1 == WithApp a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Lam a1 b1 c1 == Lam a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
AbsurdLam a1 b1 == AbsurdLam a2 b2 = (a1, b1) == (a2, b2)
ExtendedLam a1 b1 c1 d1 == ExtendedLam a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
Pi a1 b1 c1 == Pi a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Generalized a1 b1 == Generalized a2 b2 = (a1, b1) == (a2, b2)
Fun a1 b1 c1 == Fun a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Set a1 b1 == Set a2 b2 = (a1, b1) == (a2, b2)
Prop a1 b1 == Prop a2 b2 = (a1, b1) == (a2, b2)
Let a1 b1 c1 == Let a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
ETel a1 == ETel a2 = a1 == a2
Rec a1 b1 == Rec a2 b2 = (a1, b1) == (a2, b2)
RecUpdate a1 b1 c1 == RecUpdate a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Quote a1 == Quote a2 = a1 == a2
QuoteTerm a1 == QuoteTerm a2 = a1 == a2
Unquote a1 == Unquote a2 = a1 == a2
Tactic a1 b1 c1 == Tactic a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
DontCare a1 == DontCare a2 = a1 == a2
_ == _ = False
instance Eq Declaration where
ScopedDecl _ a1 == ScopedDecl _ a2 = a1 == a2
Axiom a1 b1 c1 d1 e1 f1 == Axiom a2 b2 c2 d2 e2 f2 = (a1, b1, c1, d1, e1, f1) == (a2, b2, c2, d2, e2, f2)
Generalize a1 b1 c1 d1 e1 == Generalize a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
Field a1 b1 c1 == Field a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Primitive a1 b1 c1 == Primitive a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Mutual a1 b1 == Mutual a2 b2 = (a1, b1) == (a2, b2)
Section a1 b1 c1 d1 == Section a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
Apply a1 b1 c1 d1 e1 == Apply a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
Import a1 b1 c1 == Import a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
Pragma a1 b1 == Pragma a2 b2 = (a1, b1) == (a2, b2)
Open a1 b1 c1 == Open a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
FunDef a1 b1 c1 d1 == FunDef a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
DataSig a1 b1 c1 d1 == DataSig a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
DataDef a1 b1 c1 d1 e1 == DataDef a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
RecSig a1 b1 c1 d1 == RecSig a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
RecDef a1 b1 c1 d1 e1 f1 g1 h1 i1 == RecDef a2 b2 c2 d2 e2 f2 g2 h2 i2 = (a1, b1, c1, d1, e1, f1, g1, h1, i1) == (a2, b2, c2, d2, e2, f2, g2, h2, i2)
PatternSynDef a1 b1 c1 == PatternSynDef a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
UnquoteDecl a1 b1 c1 d1 == UnquoteDecl a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
UnquoteDef a1 b1 c1 == UnquoteDef a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
_ == _ = False
instance Underscore Expr where
underscore = Underscore emptyMetaInfo
isUnderscore = __IMPOSSIBLE__
instance LensHiding LamBinding where
getHiding (DomainFree _ x) = getHiding x
getHiding (DomainFull tb) = getHiding tb
mapHiding f (DomainFree t x) = DomainFree t $ mapHiding f x
mapHiding f (DomainFull tb) = DomainFull $ mapHiding f tb
instance LensHiding TypedBinding where
getHiding (TBind _ _ (x : _) _) = getHiding x
getHiding (TBind _ _ [] _) = __IMPOSSIBLE__
getHiding TLet{} = mempty
mapHiding f (TBind r t xs e) = TBind r t ((map . mapHiding) f xs) e
mapHiding f b@TLet{} = b
instance HasRange a => HasRange (Binder' a) where
getRange (Binder p n) = fuseRange p n
instance HasRange LamBinding where
getRange (DomainFree _ x) = getRange x
getRange (DomainFull b) = getRange b
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 (Proj _ x) = getRange x
getRange (Con x) = getRange x
getRange (Lit l) = getRange l
getRange (QuestionMark i _) = getRange i
getRange (Underscore i) = getRange i
getRange (Dot 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 (Generalized _ x) = getRange x
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 (Quote i) = getRange i
getRange (QuoteTerm i) = getRange i
getRange (Unquote i) = getRange i
getRange (Tactic i _ _) = getRange i
getRange (DontCare{}) = noRange
getRange (PatternSyn x) = getRange x
getRange (Macro x) = getRange x
instance HasRange Declaration where
getRange (Axiom _ i _ _ _ _ ) = getRange i
getRange (Generalize _ 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
getRange (UnquoteDecl _ i _ _) = getRange i
getRange (UnquoteDef i _ _) = getRange i
instance HasRange (Pattern' e) where
getRange (VarP x) = getRange x
getRange (ConP i _ _) = getRange i
getRange (ProjP i _ _) = getRange i
getRange (DefP i _ _) = getRange i
getRange (WildP 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
getRange (RecP i _) = getRange i
getRange (EqualP i _) = getRange i
getRange (WithP 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 lhscore ps) = d `fuseRange` lhscore `fuseRange` ps
getRange (LHSWith h wps ps) = h `fuseRange` wps `fuseRange` ps
instance HasRange a => HasRange (Clause' a) where
getRange (Clause lhs _ rhs ds catchall) = 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 xes _ rhs wh) = getRange (xes, rhs, wh)
instance HasRange WhereDeclarations where
getRange (WhereDecls _ ds) = getRange ds
instance HasRange LetBinding where
getRange (LetBind i _ _ _ _ ) = getRange i
getRange (LetPatBind i _ _ ) = getRange i
getRange (LetApply i _ _ _ _ ) = getRange i
getRange (LetOpen i _ _ ) = getRange i
getRange (LetDeclaredVariable x) = getRange x
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 (ProjP _ o ns) = ProjP (PatRange r) o ns
setRange r (DefP _ ns as) = DefP (PatRange r) ns as
setRange r (WildP _) = WildP (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) n as
setRange r (RecP i as) = RecP (PatRange r) as
setRange r (EqualP _ es) = EqualP (PatRange r) es
setRange r (WithP i p) = WithP (setRange r i) p
instance KillRange a => KillRange (Binder' a) where
killRange (Binder a b) = killRange2 Binder a b
instance KillRange LamBinding where
killRange (DomainFree t x) = killRange2 DomainFree t x
killRange (DomainFull b) = killRange1 DomainFull b
instance KillRange GeneralizeTelescope where
killRange (GeneralizeTel s tel) = GeneralizeTel s (killRange tel)
instance KillRange DataDefParams where
killRange (DataDefParams s tel) = DataDefParams s (killRange tel)
instance KillRange TypedBinding where
killRange (TBind r t xs e) = killRange4 TBind r t 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 (Proj o x) = killRange1 (Proj o) 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 (Dot i e) = killRange2 Dot i e
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) = killRange2 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 (Generalized s x) = killRange1 (Generalized s) x
killRange (Fun i a b) = killRange3 Fun i a b
killRange (Set i n) = killRange2 Set i n
killRange (Prop i n) = killRange2 Prop i n
killRange (Let i ds e) = killRange3 Let i ds e
killRange (Rec i fs) = killRange2 Rec i fs
killRange (RecUpdate i e fs) = killRange3 RecUpdate i e fs
killRange (ETel tel) = killRange1 ETel tel
killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e
killRange (Quote i) = killRange1 Quote i
killRange (QuoteTerm i) = killRange1 QuoteTerm i
killRange (Unquote i) = killRange1 Unquote i
killRange (Tactic i e xs) = killRange3 Tactic i e xs
killRange (DontCare e) = killRange1 DontCare e
killRange (PatternSyn x) = killRange1 PatternSyn x
killRange (Macro x) = killRange1 Macro x
instance KillRange Declaration where
killRange (Axiom p i a b c d ) = killRange4 (\i a c d -> Axiom p i a b c d) i a c d
killRange (Generalize s i j x e ) = killRange4 (Generalize s) i j x e
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 ) = killRange5 Apply i a b c d
killRange (Import i a b ) = killRange3 Import i a b
killRange (Primitive i a b ) = killRange3 Primitive i a b
killRange (Pragma i a ) = Pragma (killRange i) a
killRange (Open i x dir ) = killRange3 Open i x dir
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 d ) = killRange5 DataDef i a b c d
killRange (RecSig i a b c ) = killRange4 RecSig i a b c
killRange (RecDef i a b c d e f g h) = killRange9 RecDef i a b c d e f g h
killRange (PatternSynDef x xs p ) = killRange3 PatternSynDef x xs p
killRange (UnquoteDecl mi i x e ) = killRange4 UnquoteDecl mi i x e
killRange (UnquoteDef i x e ) = killRange3 UnquoteDef i x e
instance KillRange ModuleApplication where
killRange (SectionApp a b c ) = killRange3 SectionApp a b c
killRange (RecordModuleInstance a) = killRange1 RecordModuleInstance a
instance KillRange ScopeCopyInfo where
killRange (ScopeCopyInfo a b) = killRange2 ScopeCopyInfo a b
instance KillRange e => KillRange (Pattern' e) where
killRange (VarP x) = killRange1 VarP x
killRange (ConP i a b) = killRange3 ConP i a b
killRange (ProjP i o a) = killRange3 ProjP i o a
killRange (DefP i a b) = killRange3 DefP i a b
killRange (WildP i) = killRange1 WildP 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
killRange (RecP i as) = killRange2 RecP i as
killRange (EqualP i es) = killRange2 EqualP i es
killRange (WithP i p) = killRange2 WithP i p
instance KillRange SpineLHS where
killRange (SpineLHS i a b) = killRange3 SpineLHS i a b
instance KillRange LHS where
killRange (LHS i a) = killRange2 LHS i a
instance KillRange e => KillRange (LHSCore' e) where
killRange (LHSHead a b) = killRange2 LHSHead a b
killRange (LHSProj a b c) = killRange3 LHSProj a b c
killRange (LHSWith a b c) = killRange3 LHSWith a b c
instance KillRange a => KillRange (Clause' a) where
killRange (Clause lhs spats rhs ds catchall) = killRange5 Clause lhs spats rhs ds catchall
instance KillRange ProblemEq where
killRange (ProblemEq p v a) = killRange3 ProblemEq p v a
instance KillRange RHS where
killRange AbsurdRHS = AbsurdRHS
killRange (RHS e c) = killRange2 RHS e c
killRange (WithRHS q e cs) = killRange3 WithRHS q e cs
killRange (RewriteRHS xes spats rhs wh) = killRange4 RewriteRHS xes spats rhs wh
instance KillRange WhereDeclarations where
killRange (WhereDecls a b) = killRange2 WhereDecls a b
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 ) = killRange5 LetApply i a b c d
killRange (LetOpen i x dir ) = killRange3 LetOpen i x dir
killRange (LetDeclaredVariable x) = killRange1 LetDeclaredVariable 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, Pattern' Void) |]
instanceUniverseBiT' [] [t| (Declaration, Declaration) |]
instanceUniverseBiT' [] [t| (Declaration, ModuleName) |]
instanceUniverseBiT' [] [t| (Declaration, ModuleInfo) |]
instanceUniverseBiT' [] [t| (Declaration, NamedArg LHSCore) |]
instanceUniverseBiT' [] [t| (Declaration, NamedArg BindName) |]
instanceUniverseBiT' [] [t| (Declaration, NamedArg Expr) |]
instanceUniverseBiT' [] [t| (Declaration, NamedArg Pattern) |]
instanceUniverseBiT' [] [t| (Declaration, Quantity) |]
class AllNames a where
allNames :: a -> Seq QName
instance AllNames a => AllNames [a] where
allNames = Fold.foldMap allNames
instance AllNames a => AllNames (Maybe a) where
allNames = Fold.foldMap allNames
instance AllNames a => AllNames (Arg a) where
allNames = Fold.foldMap allNames
instance AllNames a => AllNames (Named name a) where
allNames = Fold.foldMap allNames
instance (AllNames a, AllNames b) => AllNames (a,b) where
allNames (a,b) = allNames a >< allNames b
instance (AllNames a, AllNames b, AllNames c) => AllNames (a,b,c) where
allNames (a,b,c) = allNames a >< allNames b >< allNames c
instance AllNames QName where
allNames q = Seq.singleton q
instance AllNames Declaration where
allNames (Axiom _ _ _ _ q _) = Seq.singleton q
allNames (Generalize _ _ _ q _) = Seq.singleton q
allNames (Field _ q _) = Seq.singleton q
allNames (Primitive _ q _) = Seq.singleton q
allNames (Mutual _ defs) = allNames defs
allNames (DataSig _ q _ _) = Seq.singleton q
allNames (DataDef _ q _ _ decls) = q <| allNames decls
allNames (RecSig _ q _ _) = Seq.singleton q
allNames (RecDef _ q _ _ _ c _ _ decls) = q <| allNames c >< allNames decls
allNames (PatternSynDef q _ _) = Seq.singleton q
allNames (UnquoteDecl _ _ qs _) = Seq.fromList qs
allNames (UnquoteDef _ qs _) = Seq.fromList qs
allNames (FunDef _ q _ cls) = q <| allNames cls
allNames (Section _ _ _ decls) = allNames decls
allNames Apply{} = Seq.empty
allNames Import{} = Seq.empty
allNames Pragma{} = Seq.empty
allNames Open{} = Seq.empty
allNames (ScopedDecl _ decls) = allNames decls
instance AllNames Clause where
allNames cl = allNames (clauseRHS cl, clauseWhereDecls cl)
instance (AllNames qn, AllNames e) => AllNames (RewriteEqn' qn p e) where
allNames = \case
Rewrite es -> Fold.foldMap allNames es
Invert qn pes -> allNames qn >< foldMap (Fold.foldMap allNames) pes
instance AllNames RHS where
allNames (RHS e _) = allNames e
allNames AbsurdRHS{} = Seq.empty
allNames (WithRHS q _ cls) = q <| allNames cls
allNames (RewriteRHS qes _ rhs cls) = allNames (qes, rhs, cls)
instance AllNames WhereDeclarations where
allNames (WhereDecls _ ds) = allNames ds
instance AllNames Expr where
allNames Var{} = Seq.empty
allNames Def{} = Seq.empty
allNames Proj{} = Seq.empty
allNames Con{} = Seq.empty
allNames Lit{} = Seq.empty
allNames QuestionMark{} = Seq.empty
allNames Underscore{} = Seq.empty
allNames (Dot _ e) = allNames e
allNames (App _ e1 e2) = allNames e1 >< allNames e2
allNames (WithApp _ e es) = allNames e >< allNames es
allNames (Lam _ b e) = allNames b >< allNames e
allNames AbsurdLam{} = Seq.empty
allNames (ExtendedLam _ _ q cls) = q <| allNames cls
allNames (Pi _ tel e) = allNames tel >< allNames e
allNames (Generalized s e) = Seq.fromList (Set.toList s) >< allNames e
allNames (Fun _ e1 e2) = allNames e1 >< allNames e2
allNames Set{} = Seq.empty
allNames Prop{} = Seq.empty
allNames (Let _ lbs e) = allNames lbs >< allNames e
allNames ETel{} = __IMPOSSIBLE__
allNames (Rec _ fields) = allNames [ a ^. exprFieldA | Left a <- fields ]
allNames (RecUpdate _ e fs) = allNames e >< allNames (map (view exprFieldA) fs)
allNames (ScopedExpr _ e) = allNames e
allNames Quote{} = Seq.empty
allNames QuoteTerm{} = Seq.empty
allNames Unquote{} = Seq.empty
allNames (Tactic _ e xs) = allNames e >< allNames xs
allNames DontCare{} = Seq.empty
allNames PatternSyn{} = Seq.empty
allNames Macro{} = Seq.empty
instance AllNames LamBinding where
allNames DomainFree{} = Seq.empty
allNames (DomainFull binds) = allNames binds
instance AllNames TypedBinding where
allNames (TBind _ t _ e) = allNames (t, e)
allNames (TLet _ lbs) = allNames lbs
instance AllNames LetBinding where
allNames (LetBind _ _ _ e1 e2) = allNames e1 >< allNames e2
allNames (LetPatBind _ _ e) = allNames e
allNames (LetApply _ _ app _ _) = allNames app
allNames LetOpen{} = Seq.empty
allNames (LetDeclaredVariable _) = Seq.empty
instance AllNames ModuleApplication where
allNames (SectionApp bindss _ es) = allNames bindss >< allNames es
allNames RecordModuleInstance{} = Seq.empty
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__
class NameToExpr a where
nameToExpr :: a -> Expr
instance NameToExpr AbstractName where
nameToExpr d =
case anameKind d of
DataName -> Def x
RecName -> Def x
AxiomName -> Def x
PrimName -> Def x
FunName -> Def x
OtherDefName -> Def x
GeneralizeName -> Def x
DisallowedGeneralizeName -> Def x
FldName -> Proj ProjSystem ux
ConName -> Con ux
PatternSynName -> PatternSyn ux
MacroName -> Macro x
QuotableName -> App (defaultAppInfo r) (Quote i) (defaultNamedArg $ Def x)
where
x = anameName d
ux = unambiguous x
r = getRange x
i = ExprRange r
instance NameToExpr ResolvedName where
nameToExpr = \case
VarName x _ -> Var x
DefinedName _ x -> nameToExpr x
FieldName xs -> Proj ProjSystem . AmbQ . fmap anameName $ xs
ConstructorName xs -> Con . AmbQ . fmap anameName $ xs
PatternSynResName xs -> PatternSyn . AmbQ . fmap anameName $ xs
UnknownName -> __IMPOSSIBLE__
app :: Expr -> [NamedArg Expr] -> Expr
app = foldl (App defaultAppInfo_)
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkLet i [] e = e
mkLet i ds e = Let i ds e
patternToExpr :: Pattern -> Expr
patternToExpr = \case
VarP x -> Var (unBind x)
ConP _ c ps -> Con c `app` map (fmap (fmap patternToExpr)) ps
ProjP _ o ds -> Proj o ds
DefP _ fs ps -> Def (headAmbQ fs) `app` map (fmap (fmap patternToExpr)) ps
WildP _ -> Underscore emptyMetaInfo
AsP _ _ p -> patternToExpr p
DotP _ e -> e
AbsurdP _ -> Underscore emptyMetaInfo
LitP l -> Lit l
PatternSynP _ c ps -> PatternSyn c `app` (map . fmap . fmap) patternToExpr ps
RecP _ as -> Rec exprNoRange $ map (Left . fmap patternToExpr) as
EqualP{} -> __IMPOSSIBLE__
WithP r p -> __IMPOSSIBLE__
type PatternSynDefn = ([Arg Name], Pattern' Void)
type PatternSynDefns = Map QName PatternSynDefn
lambdaLiftExpr :: [Name] -> Expr -> Expr
lambdaLiftExpr [] e = e
lambdaLiftExpr (n:ns) e =
Lam exprNoRange (mkDomainFree $ defaultNamedArg $ mkBinder_ n) $
lambdaLiftExpr ns e
class SubstExpr a where
substExpr :: [(Name, Expr)] -> a -> a
instance SubstExpr a => SubstExpr (Maybe a) where
substExpr = fmap . substExpr
instance SubstExpr a => SubstExpr [a] where
substExpr = fmap . substExpr
instance SubstExpr a => SubstExpr (Arg a) where
substExpr = fmap . substExpr
instance SubstExpr a => SubstExpr (Named name a) where
substExpr = fmap . substExpr
instance (SubstExpr a, SubstExpr b) => SubstExpr (a, b) where
substExpr s (x, y) = (substExpr s x, substExpr s y)
instance (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) where
substExpr s (Left x) = Left (substExpr s x)
substExpr s (Right y) = Right (substExpr s y)
instance SubstExpr C.Name where
substExpr _ = id
instance SubstExpr ModuleName where
substExpr _ = id
instance SubstExpr Assign where
substExpr s (FieldAssignment n x) = FieldAssignment n (substExpr s x)
instance SubstExpr Expr where
substExpr s e = case e of
Var n -> fromMaybe e (lookup n s)
Def _ -> e
Proj{} -> e
Con _ -> e
Lit _ -> e
QuestionMark{} -> e
Underscore _ -> e
Dot i e -> Dot i (substExpr s e)
App i e e' -> App i (substExpr s e) (substExpr s e')
WithApp i e es -> WithApp i (substExpr s e) (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 (substExpr s t) (substExpr s e)
Generalized ns e -> Generalized ns (substExpr s e)
Fun i ae e -> Fun i (substExpr s ae) (substExpr s e)
Set i n -> e
Prop i n -> e
Let i ls e -> Let i (substExpr s ls) (substExpr s e)
ETel t -> e
Rec i nes -> Rec i (substExpr s nes)
RecUpdate i e nes -> RecUpdate i (substExpr s e) (substExpr s nes)
ScopedExpr si e -> ScopedExpr si (substExpr s e)
Quote i -> e
QuoteTerm i -> e
Unquote i -> e
Tactic i e xs -> Tactic i (substExpr s e) (substExpr s xs)
DontCare e -> DontCare (substExpr s e)
PatternSyn{} -> e
Macro{} -> e
instance SubstExpr LetBinding where
substExpr 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
instance SubstExpr TypedBinding where
substExpr s tb = case tb of
TBind r t ns e -> TBind r (substExpr s t) ns $ substExpr s e
TLet r lbs -> TLet r $ substExpr 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')
| visible n = Nothing
| otherwise = return (wild r, as)
matchNext _ [] = False
matchNext n (a:as) = sameHiding n a && maybe True (x ==) (bareNameOf a)
where
x = C.nameToRawName $ nameConcrete $ unArg n
matchArgs r [] [] = return ([], [])
matchArgs r [] as = Nothing
matchArgs r (n:ns) [] | visible n = return ([], n : ns)
matchArgs r (n:ns) as = do
(p, as) <- matchNextArg r n as
first ((unArg n, p) :) <$> matchArgs (getRange p) ns as