{-# LANGUAGE CPP #-}
{-# 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, second, (***))
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.Traversable
import Data.Void
import Data.Data (Data)
import Data.Monoid (mappend)
import Agda.Syntax.Concrete.Name (NumHoles(..))
import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA, HoleContent'(..))
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pretty ()
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.Fixity ( Fixity' )
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.Functor
import Agda.Utils.Geniplate
import Agda.Utils.Lens
import Agda.Utils.NonemptyList
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
newtype BindName = BindName { unBind :: Name }
deriving (Show, Data, HasRange, SetRange, KillRange)
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
| QuoteGoal ExprInfo Name Expr
| QuoteContext ExprInfo
| Quote ExprInfo
| QuoteTerm ExprInfo
| Unquote ExprInfo
| Tactic ExprInfo Expr [NamedArg 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)
class GetDefInfo a where
getDefInfo :: a -> Maybe DefInfo
instance GetDefInfo Declaration where
getDefInfo (Axiom _ i _ _ _ _) = Just i
getDefInfo (Generalize _ 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
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 String ResolvedName
| BuiltinNoDefPragma String QName
| RewritePragma QName
| CompilePragma String 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
data LamBinding
= DomainFree (NamedArg BindName)
| DomainFull TypedBinding
deriving (Data, Show, Eq)
data TypedBinding
= TBind Range [NamedArg BindName] Expr
| TLet Range [LetBinding]
deriving (Data, Show, Eq)
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 :: 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
data RHS
= RHS
{ rhsExpr :: Expr
, rhsConcrete :: Maybe C.Expr
}
| AbsurdRHS
| WithRHS QName [Expr] [Clause]
| RewriteRHS
{ rewriteExprs :: [(QName, Expr)]
, 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' 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)
QuoteGoal a1 b1 c1 == QuoteGoal a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2)
QuoteContext a1 == QuoteContext a2 = a1 == a2
Quote a1 == Quote a2 = a1 == a2
QuoteTerm a1 == QuoteTerm a2 = a1 == a2
Unquote a1 == Unquote a2 = a1 == a2
Tactic a1 b1 c1 d1 == Tactic a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2)
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 x) = DomainFree $ 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 xs e) = TBind r ((map . mapHiding) f xs) e
mapHiding f b@TLet{} = b
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 (QuoteGoal _ _ e) = getRange e
getRange (QuoteContext i) = getRange i
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 (map snd 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 LamBinding where
killRange (DomainFree x) = killRange1 DomainFree 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 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 (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 (QuoteGoal i x e) = killRange3 QuoteGoal i x e
killRange (QuoteContext i) = killRange1 QuoteContext i
killRange (Quote i) = killRange1 Quote i
killRange (QuoteTerm i) = killRange1 QuoteTerm i
killRange (Unquote i) = killRange1 Unquote i
killRange (Tactic i e xs ys) = killRange4 Tactic i e xs ys
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) |]
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 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 RHS where
allNames (RHS e _) = allNames e
allNames AbsurdRHS{} = Seq.empty
allNames (WithRHS q _ cls) = q <| allNames cls
allNames (RewriteRHS qes _ rhs cls) = Seq.fromList (map fst qes) >< allNames rhs >< allNames 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 (QuoteGoal _ _ e) = allNames e
allNames (QuoteContext _) = Seq.empty
allNames Quote{} = Seq.empty
allNames QuoteTerm{} = Seq.empty
allNames Unquote{} = Seq.empty
allNames (Tactic _ e xs ys) = allNames e >< allNames xs >< allNames ys
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 _ _ e) = allNames 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
nameExpr :: a -> Expr
instance NameToExpr AbstractName where
nameExpr d = mk (anameKind d) $ anameName d
where
mk DefName x = Def x
mk GeneralizeName x = Def x
mk DisallowedGeneralizeName x = Def x
mk FldName x = Proj ProjSystem $ unambiguous x
mk ConName x = Con $ unambiguous x
mk PatternSynName x = PatternSyn $ unambiguous x
mk MacroName x = Macro x
mk QuotableName x = App (defaultAppInfo r) (Quote i) (defaultNamedArg $ Def x)
where i = ExprRange r
r = getRange x
instance NameToExpr ResolvedName where
nameExpr = \case
VarName x _ -> Var x
DefinedName _ x -> nameExpr 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 (VarP x) = Var (unBind x)
patternToExpr (ConP _ c ps) =
Con c `app` map (fmap (fmap patternToExpr)) ps
patternToExpr (ProjP _ o ds) = Proj o ds
patternToExpr (DefP _ fs ps) =
Def (headAmbQ fs) `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 (PatternSynP _ c ps) = PatternSyn c `app` (map . fmap . fmap) patternToExpr ps
patternToExpr (RecP _ as) = Rec exprNoRange $ map (Left . fmap patternToExpr) as
patternToExpr EqualP{} = __IMPOSSIBLE__
patternToExpr (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 (DomainFree $ defaultNamedArg $ BindName n) $
lambdaLiftExpr ns e
class SubstExpr a where
substExpr :: [(Name, Expr)] -> a -> a
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)
QuoteGoal i n e -> QuoteGoal i n (substExpr s e)
QuoteContext i -> e
Quote i -> e
QuoteTerm i -> e
Unquote i -> e
Tactic i e xs ys -> Tactic i (substExpr s e) (substExpr s xs) (substExpr s ys)
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 ns e -> TBind r 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 && matchName
where
x = unranged $ C.nameToRawName $ nameConcrete $ unArg n
matchName = maybe True (== x) (nameOf $ unArg a)
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