| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Abstract
Synopsis
- data WhatName
- data Name = Name {}
- fresh :: String -> Name
- freshen :: Name -> Name
- noName :: Name
- emptyName :: Name -> Bool
- nonEmptyName :: Name -> String -> Name
- bestName :: [Name] -> Name
- iAmNotUnique :: Unique
- unsafeName :: String -> Name
- mkExtName :: Name -> Name
- mkExtRef :: Name -> Expr
- isEtaAlias :: Name -> Bool
- internal :: Name -> Name
- spaceToUnderscore :: String -> String
- data QName
- nameInstanceOf :: QName -> QName -> Bool
- unqual :: QName -> Name
- data Sized
- data Co
- showFun :: Co -> String
- data LtLe
- data Decoration pos
- = Dec {
- thePolarity :: pos
- | Hidden
- = Dec {
- polarity :: Polarity pol => Decoration pol -> pol
- type Dec = Decoration Pol
- type UDec = Decoration PProd
- class LensPol a where
- udec :: Dec -> UDec
- irrelevantDec :: Decoration Pol
- paramDec :: Decoration Pol
- defaultDec :: Decoration Pol
- defaultUpperDec :: Decoration PProd
- neutralDec :: Decoration Pol
- coDomainDec :: Dec -> Dec
- compDec :: Dec -> UDec -> UDec
- class HasPred a where
- predecessor :: a -> Maybe a
- sizeSuccE :: Expr -> Expr
- minSizeE :: Expr -> Expr -> Expr
- maxSizeE :: Expr -> Expr -> Expr
- flattenMax :: Expr -> [Expr] -> [Expr]
- maxE :: [Expr] -> Expr
- sizeVarsToInfty :: Expr -> Expr
- leqSizeE :: Expr -> Expr -> Bool
- data Class
- predClass :: Class -> Class
- data Sort a
- topSort :: Sort Expr
- tSize :: Expr
- isSize :: Expr -> Bool
- predSort :: Sort Expr -> Sort Expr
- succSort :: Sort Expr -> Sort Expr
- minSort :: Sort Expr -> Sort Expr -> Sort Expr
- minClass :: Class -> Class -> Class
- maxClass :: Class -> Class -> Class
- maxSort :: Sort Expr -> Sort Expr -> Sort Expr
- irrSortFor :: Sort Expr -> Sort Expr -> Bool
- data Kind
- defaultKind :: Kind
- preciseKind :: Sort Expr -> Kind
- kSize :: Kind
- kTSize :: Kind
- kTerm :: Kind
- kType :: Kind
- kUniv :: Expr -> Kind
- prettyKind :: Kind -> String
- dataKind :: Kind -> Kind
- argKind :: Kind -> Kind
- predKind :: Kind -> Kind
- succKind :: Kind -> Kind
- intersectKind :: Kind -> Kind -> Kind
- unionKind :: Kind -> Kind -> Kind
- irrelevantFor :: Kind -> Kind -> Bool
- data Kinded a = Kinded {}
- data Dom a = Domain {}
- defaultDomain :: a -> Dom a
- domFromKinded :: Kinded a -> Dom a
- defaultIrrDom :: a -> Dom a
- sizeDomain :: Dec -> Dom Expr
- belowDomain :: Dec -> LtLe -> Expr -> Dom Expr
- class LensDec a where
- data ConK
- data IdKind
- conKind :: IdKind -> Bool
- coToConK :: Co -> ConK
- data DefId = DefId {}
- type MVar = Int
- data TBinding a
- type LBind = TBinding (Maybe Type)
- type TBind = TBinding Type
- noBind :: Dom a -> TBinding a
- boundType :: TBind -> Type
- mapDecM :: Applicative m => (Dec -> m Dec) -> TBind -> m TBind
- newtype Measure a = Measure {
- measure :: [a]
- succMeasure :: (a -> a) -> Measure a -> Measure a
- applyLastM :: (a -> Maybe a) -> Measure a -> Maybe (Measure a)
- data Bound a = Bound {}
- data Tag
- type Tags = [Tag]
- inTags :: Tag -> Tags -> Bool
- noTags :: Tags
- data Tagged a = Tagged {}
- showCast :: Bool -> String -> String
- prettyErased :: Bool -> Doc -> Doc
- prettyCast :: Bool -> Doc -> Doc
- data Expr
- = Sort (Sort Expr)
- | Zero
- | Succ Expr
- | Infty
- | Max [Expr]
- | Plus [Expr]
- | Meta MVar
- | Var Name
- | Def DefId
- | Record RecInfo [(Name, Expr)]
- | Proj PrePost Name
- | Pair Expr Expr
- | Case Expr (Maybe Type) [Clause]
- | LLet LBind Telescope Expr Expr
- | App Expr Expr
- | Lam Dec Name Expr
- | Quant PiSigma TBind Expr
- | Sing Expr Expr
- | Below LtLe Expr
- | Ann (Tagged Expr)
- | Irr
- data PrePost
- data PiSigma
- data RecInfo
- = AnonRec
- | NamedRec {
- recConK :: ConK
- recConName :: QName
- recNamedFields :: Bool
- recDottedRef :: Dotted
- newtype Dotted = Dotted {}
- mkDotted :: MonadIO m => Bool -> m Dotted
- notDotted :: Dotted
- isDotted :: Dotted -> Bool
- clearDotted :: MonadIO m => Dotted -> m ()
- alignDotted :: MonadIO m => Dotted -> Dotted -> m ()
- recDotted :: RecInfo -> Bool
- pi :: TBind -> Expr -> Expr
- piSig :: PiSigma -> TBind -> Expr -> Expr
- proj :: Expr -> PrePost -> Name -> Expr
- funType :: Dom Type -> Expr -> Expr
- erasedExpr :: Expr -> Expr
- castExpr :: Expr -> Expr
- succView :: Expr -> (Int, Expr)
- data Clause = Clause {}
- clause :: [Pattern] -> Maybe Expr -> Clause
- data PatternInfo = PatternInfo {}
- type Pattern = Pat Expr
- data Pat e
- type Case = (Pattern, Expr)
- type Subst = Map MVar Expr
- con :: ConK -> QName -> Expr
- fun :: QName -> Expr
- dat :: QName -> Expr
- letdef :: Name -> Expr
- type SpineView = (Expr, [Expr])
- spineView :: Expr -> SpineView
- test_spineView :: SpineView
- isErasedExpr :: Expr -> (Bool, Expr)
- type Extr = Expr
- type EType = Type
- data Declaration
- = DataDecl Name Sized Co [Pol] Telescope Type [Constructor] [Name]
- | RecordDecl Name Telescope Type Constructor [Name]
- | MutualFunDecl Bool Co [Fun]
- | FunDecl Co Fun
- | LetDecl Bool Name Telescope (Maybe Type) Expr
- | PatternDecl Name [Name] Pattern
- | MutualDecl Bool [Declaration]
- | OverrideDecl Override [Declaration]
- data Override
- = Fail
- | Check
- | TrustMe
- | Impredicative
- data TySig a = TypeSig {}
- type TypeSig = TySig Type
- type Type = Expr
- data Constructor = Constructor {}
- type ParamPats = Maybe (Telescope, [Pattern])
- newtype Telescope = Telescope {}
- emptyTel :: Telescope
- data Arity = Arity {
- fullArity :: Int
- isProjection :: Maybe Int
- data Fun = Fun {
- funTypeSig :: TypeSig
- funExtName :: Name
- funArity :: Arity
- funClauses :: [Clause]
- type EDeclaration = Declaration
- type EClause = Clause
- type EPattern = Pattern
- type EConstructor = Constructor
- type ETypeSig = TypeSig
- type EFun = Fun
- type ETelescope = Telescope
- eraseMeasure :: Expr -> Expr
- inferable :: Expr -> Bool
- class BoundVars a where
- boundVars :: Collection c Name => a -> c
- class FreeVars a where
- patternVars :: Pattern -> [Name]
- class UsedDefs a where
- rhsDefs :: [Clause] -> [Name]
- precAppL :: Int
- precAppR :: Int
- precArrL :: Int
- class DotIf a where
- prettyRecFields :: (Pretty a, Pretty b) => [(a, b)] -> Doc
- prettyCase :: Clause -> Doc
- vlist :: [Doc] -> Doc
- showCase :: Clause -> String
- showCases :: [Clause] -> String
- patSubst :: [(Name, Pattern)] -> Pattern -> Pattern
- class ParSubst a where
- class Substitute a where
- prettyFun :: Name -> [Clause] -> Doc
- prettyClause :: Pretty a => a -> Clause -> Doc
- data FieldClass
- type Destructor = (Type, Arity, Clause)
- data FieldInfo = FieldInfo {}
- data PatternsType
- data ConstructorInfo = ConstructorInfo {}
- corePat :: ConstructorInfo -> [Pattern]
- class InjectiveVars a where
- injectiveVars :: a -> Set Name
- classifyFields :: Co -> Name -> Type -> [FieldInfo]
- isField :: FieldClass -> Bool
- isNamedField :: FieldInfo -> Bool
- destructorNames :: [FieldInfo] -> [Name]
- analyzeConstructor :: Co -> Name -> Telescope -> Constructor -> ConstructorInfo
- destructorNamesPresent :: [FieldInfo] -> Bool
- analyzeConstructors :: Co -> Name -> Telescope -> [Constructor] -> [ConstructorInfo]
- reassembleConstructor :: ConstructorInfo -> Constructor
- reassembleConstructorType :: ConstructorInfo -> Type
- isPatIndFamC :: Expr -> Writer All [Pattern]
- tsoFromPatterns :: [Pattern] -> TSO Name
- overlap :: Pattern -> Pattern -> Bool
- overlaps :: [Pattern] -> [Pattern] -> Bool
- exprToPattern :: Expr -> Maybe Pattern
- patApp :: Pattern -> Pattern -> Maybe Pattern
- exprToDotPat :: Expr -> (Bool, Pattern)
- exprToDotPat' :: Expr -> Writer All Pattern
- patternToExpr :: Pattern -> Expr
- dotConstructors :: Pattern -> Pattern
- completeP :: Pattern -> Bool
- isDotPattern :: Pattern -> Bool
- isSuccessorPattern :: Pattern -> Bool
- isSuccessor :: Expr -> Bool
- shallowSuccP :: Pattern -> Bool
- typeToTele :: Type -> (Telescope, Type)
- typeToTele' :: Int -> Type -> (Telescope, Type)
- teleLam :: Telescope -> Expr -> Expr
- teleToType' :: (Dec -> Dec) -> Telescope -> Type -> Type
- teleToType :: Telescope -> Type -> Type
- teleToTypeErase :: Telescope -> Type -> Type
- adjustTopDecs :: (Dec -> Dec) -> Type -> Type
- teleToTypeM :: Applicative m => (Dec -> m Dec) -> Telescope -> Type -> m Type
- adjustTopDecsM :: Applicative m => (Dec -> m Dec) -> Type -> m Type
Names carry a name suggestion and a unique identifier
Constructors
| UserName | |
| EtaAliasName | a name for the eta-expanded name of a definition |
| QuoteName |
Constructors
| Name | |
fresh :: String -> Name Source #
fresh s generates a new name with suggestion s.
To a void a monad here, we use imperative features (unsafePerformIO).
unsafeName :: String -> Name Source #
isEtaAlias :: Name -> Bool Source #
spaceToUnderscore :: String -> String Source #
Convert a dot pattern into an identifier which should not look too confusing.
Qualified name.
nameInstanceOf :: QName -> QName -> Bool Source #
An unqualified name is an instance of a qualified name.
data Decoration pos Source #
Constructors
| Dec | |
Fields
| |
| Hidden | |
Instances
polarity :: Polarity pol => Decoration pol -> pol Source #
type Dec = Decoration Pol Source #
type UDec = Decoration PProd Source #
class LensPol a where Source #
Minimal complete definition
paramDec :: Decoration Pol Source #
neutralDec :: Decoration Pol Source #
Composing with neutralDec should do nothing.
coDomainDec :: Dec -> Dec Source #
class HasPred a where Source #
Methods
predecessor :: a -> Maybe a Source #
sizeVarsToInfty :: Expr -> Expr Source #
Instances
defaultKind :: Kind Source #
prettyKind :: Kind -> String Source #
Instances
| Functor Kinded Source # | |
| Foldable Kinded Source # | |
Defined in Abstract Methods fold :: Monoid m => Kinded m -> m # foldMap :: Monoid m => (a -> m) -> Kinded a -> m # foldMap' :: Monoid m => (a -> m) -> Kinded a -> m # foldr :: (a -> b -> b) -> b -> Kinded a -> b # foldr' :: (a -> b -> b) -> b -> Kinded a -> b # foldl :: (b -> a -> b) -> b -> Kinded a -> b # foldl' :: (b -> a -> b) -> b -> Kinded a -> b # foldr1 :: (a -> a -> a) -> Kinded a -> a # foldl1 :: (a -> a -> a) -> Kinded a -> a # elem :: Eq a => a -> Kinded a -> Bool # maximum :: Ord a => Kinded a -> a # minimum :: Ord a => Kinded a -> a # | |
| Traversable Kinded Source # | |
| Show a => Show (Kinded a) Source # | |
| Eq a => Eq (Kinded a) Source # | |
| Ord a => Ord (Kinded a) Source # | |
Defined in Abstract | |
Instances
defaultDomain :: a -> Dom a Source #
domFromKinded :: Kinded a -> Dom a Source #
defaultIrrDom :: a -> Dom a Source #
class LensDec a where Source #
Minimal complete definition
Instances
Instances
succMeasure :: (a -> a) -> Measure a -> Measure a Source #
Instances
Instances
Constructors
| Sort (Sort Expr) |
|
| Zero | |
| Succ Expr | |
| Infty | |
| Max [Expr] | (list has at least 2 elements) |
| Plus [Expr] | (list has at least 2 elements) identifiers |
| Meta MVar | meta-variable |
| Var Name | variables are named |
| Def DefId | identifiers in the signature |
| Record RecInfo [(Name, Expr)] | record { p1 = e1; ...; pn = en } |
| Proj PrePost Name | proj _ or _ .proj |
| Pair Expr Expr | |
| Case Expr (Maybe Type) [Clause] | Type is |
| LLet LBind Telescope Expr Expr |
|
| App Expr Expr | |
| Lam Dec Name Expr | |
| Quant PiSigma TBind Expr | |
| Sing Expr Expr | |
| Below LtLe Expr | <(a : Size) or <=(a : Size) for extraction |
| Ann (Tagged Expr) | annotated expr, e.g. with Erased tag |
| Irr | for instance the term correponding to the absurd pattern |
Instances
Optional constructor name of a record value.
Constructors
| AnonRec | anonymous record |
| NamedRec | |
Fields
| |
clearDotted :: MonadIO m => Dotted -> m () Source #
smart constructors
erasedExpr :: Expr -> Expr Source #
data PatternInfo Source #
Constructors
| PatternInfo | |
Instances
| Show PatternInfo Source # | |
Defined in Abstract Methods showsPrec :: Int -> PatternInfo -> ShowS # show :: PatternInfo -> String # showList :: [PatternInfo] -> ShowS # | |
| Eq PatternInfo Source # | |
Defined in Abstract | |
| Ord PatternInfo Source # | |
Defined in Abstract Methods compare :: PatternInfo -> PatternInfo -> Ordering # (<) :: PatternInfo -> PatternInfo -> Bool # (<=) :: PatternInfo -> PatternInfo -> Bool # (>) :: PatternInfo -> PatternInfo -> Bool # (>=) :: PatternInfo -> PatternInfo -> Bool # max :: PatternInfo -> PatternInfo -> PatternInfo # min :: PatternInfo -> PatternInfo -> PatternInfo # | |
Patterns parametrized by type of dot patterns.
Constructors
| VarP Name | x |
| ConP PatternInfo QName [Pat e] | (c ps) and (.c ps) |
| SuccP (Pat e) | ($ p) |
| SizeP e Name | (x > y) (# > y) ($x > y) |
| PairP (Pat e) (Pat e) | (p, p') |
| ProjP Name | .proj |
| DotP e | .e |
| AbsurdP | () |
| ErasedP (Pat e) | pattern which got erased |
| UnusableP (Pat e) |
data Declaration Source #
Constructors
| DataDecl Name Sized Co [Pol] Telescope Type [Constructor] [Name] | |
| RecordDecl Name Telescope Type Constructor [Name] | |
| MutualFunDecl Bool Co [Fun] | |
| FunDecl Co Fun | |
| LetDecl Bool Name Telescope (Maybe Type) Expr | Bool for eval. After t.c., tel. is empty and type is Just. |
| PatternDecl Name [Name] Pattern | |
| MutualDecl Bool [Declaration] | |
| OverrideDecl Override [Declaration] |
Instances
| Show Declaration Source # | |
Defined in Abstract Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS # | |
| Eq Declaration Source # | |
Defined in Abstract | |
| Ord Declaration Source # | |
Defined in Abstract Methods compare :: Declaration -> Declaration -> Ordering # (<) :: Declaration -> Declaration -> Bool # (<=) :: Declaration -> Declaration -> Bool # (>) :: Declaration -> Declaration -> Bool # (>=) :: Declaration -> Declaration -> Bool # max :: Declaration -> Declaration -> Declaration # min :: Declaration -> Declaration -> Declaration # | |
Constructors
| Fail | expect an error, ignore block |
| Check | expect no error, still ignore block |
| TrustMe | ignore recoverable errors |
| Impredicative | use impredicativity for these declarations |
data Constructor Source #
Constructor declaration. Top-level scope (independent of data pars).
Constructors
| Constructor | |
Instances
| Show Constructor Source # | |
Defined in Abstract Methods showsPrec :: Int -> Constructor -> ShowS # show :: Constructor -> String # showList :: [Constructor] -> ShowS # | |
| Eq Constructor Source # | |
Defined in Abstract | |
| Ord Constructor Source # | |
Defined in Abstract Methods compare :: Constructor -> Constructor -> Ordering # (<) :: Constructor -> Constructor -> Bool # (<=) :: Constructor -> Constructor -> Bool # (>) :: Constructor -> Constructor -> Bool # (>=) :: Constructor -> Constructor -> Bool # max :: Constructor -> Constructor -> Constructor # min :: Constructor -> Constructor -> Constructor # | |
Instances
Constructors
| Arity | |
Fields
| |
Constructors
| Fun | |
Fields
| |
type EDeclaration = Declaration Source #
type EConstructor = Constructor Source #
type ETelescope = Telescope Source #
eraseMeasure :: Expr -> Expr Source #
class BoundVars a where Source #
Collect the variables from the binders
Methods
boundVars :: Collection c Name => a -> c Source #
Instances
class FreeVars a where Source #
Boilerplate to extract free variables in the usual sense.
Instances
| FreeVars Clause Source # | |
| FreeVars Expr Source # | |
| FreeVars Telescope Source # | |
| FreeVars a => FreeVars (Bound a) Source # | |
| FreeVars a => FreeVars (Dom a) Source # | |
| FreeVars a => FreeVars (Measure a) Source # | |
| FreeVars a => FreeVars (Sort a) Source # | |
| FreeVars a => FreeVars (TBinding a) Source # | |
| FreeVars a => FreeVars (Tagged a) Source # | |
| FreeVars a => FreeVars (Maybe a) Source # | |
| FreeVars a => FreeVars [a] Source # | |
| (FreeVars a, FreeVars b) => FreeVars (a, b) Source # | |
| (FreeVars a, FreeVars b, FreeVars c) => FreeVars (a, b, c) Source # | |
patternVars :: Pattern -> [Name] Source #
class UsedDefs a where Source #
Get all the definitions that are refered to in expression. This is used e.g. to check whether a (co)fun is recursive.
Instances
| UsedDefs Clause Source # | |
| UsedDefs DefId Source # | |
| UsedDefs Expr Source # | |
| UsedDefs Telescope Source # | |
| UsedDefs a => UsedDefs (Bound a) Source # | |
| UsedDefs a => UsedDefs (Dom a) Source # | |
| UsedDefs a => UsedDefs (Measure a) Source # | |
| UsedDefs a => UsedDefs (Sort a) Source # | |
| UsedDefs a => UsedDefs (TBinding a) Source # | |
| UsedDefs a => UsedDefs (Tagged a) Source # | |
| UsedDefs a => UsedDefs (Maybe a) Source # | |
| UsedDefs a => UsedDefs [a] Source # | |
| (UsedDefs a, UsedDefs b) => UsedDefs (a, b) Source # | |
| (UsedDefs a, UsedDefs b, UsedDefs c) => UsedDefs (a, b, c) Source # | |
| (UsedDefs a, UsedDefs b, UsedDefs c, UsedDefs d) => UsedDefs (a, b, c, d) Source # | |
prettyCase :: Clause -> Doc Source #
class ParSubst a where Source #
Instances
| ParSubst Clause Source # | |
| ParSubst Expr Source # | |
| ParSubst Telescope Source # | |
| ParSubst a => ParSubst (Bound a) Source # | |
| ParSubst a => ParSubst (Dom a) Source # | |
| ParSubst a => ParSubst (Measure a) Source # | |
| ParSubst a => ParSubst (Sort a) Source # | |
| ParSubst a => ParSubst (TBinding a) Source # | |
| ParSubst a => ParSubst (Tagged a) Source # | |
| ParSubst a => ParSubst (Maybe a) Source # | |
| ParSubst a => ParSubst [a] Source # | |
class Substitute a where Source #
Metavariable substitution. (BY INTENTION NOT CAPTURE AVOIDING!) Does not substitute in patterns!
Instances
| Substitute Clause Source # | |
| Substitute Expr Source # | |
| Substitute Telescope Source # | |
| Substitute a => Substitute (Bound a) Source # | |
| Substitute a => Substitute (Dom a) Source # | |
| Substitute a => Substitute (Measure a) Source # | |
| Substitute a => Substitute (Sort a) Source # | |
| Substitute a => Substitute (TBinding a) Source # | |
| Substitute a => Substitute (Tagged a) Source # | |
| Substitute a => Substitute (Maybe a) Source # | |
| Substitute a => Substitute [a] Source # | |
data FieldClass Source #
Constructors
| Index | E.g., the length in Vector. |
| NotErasableIndex | E.g., |
| Field (Maybe Destructor) | An actual field, not free in the target. |
Instances
| Show FieldClass Source # | |
Defined in Abstract Methods showsPrec :: Int -> FieldClass -> ShowS # show :: FieldClass -> String # showList :: [FieldClass] -> ShowS # | |
| Eq FieldClass Source # | |
Defined in Abstract | |
Constructors
| FieldInfo | |
data PatternsType Source #
Constructors
| NotPatterns | |
| LinearPatterns | |
| NonLinearPatterns |
Instances
| Show PatternsType Source # | |
Defined in Abstract Methods showsPrec :: Int -> PatternsType -> ShowS # show :: PatternsType -> String # showList :: [PatternsType] -> ShowS # | |
| Eq PatternsType Source # | |
Defined in Abstract | |
| Ord PatternsType Source # | |
Defined in Abstract Methods compare :: PatternsType -> PatternsType -> Ordering # (<) :: PatternsType -> PatternsType -> Bool # (<=) :: PatternsType -> PatternsType -> Bool # (>) :: PatternsType -> PatternsType -> Bool # (>=) :: PatternsType -> PatternsType -> Bool # max :: PatternsType -> PatternsType -> PatternsType # min :: PatternsType -> PatternsType -> PatternsType # | |
data ConstructorInfo Source #
Constructors
| ConstructorInfo | |
Instances
| Show ConstructorInfo Source # | |
Defined in Abstract Methods showsPrec :: Int -> ConstructorInfo -> ShowS # show :: ConstructorInfo -> String # showList :: [ConstructorInfo] -> ShowS # | |
corePat :: ConstructorInfo -> [Pattern] Source #
class InjectiveVars a where Source #
Methods
injectiveVars :: a -> Set Name Source #
Instances
| InjectiveVars Expr Source # | |
| InjectiveVars Telescope Source # | |
| InjectiveVars a => InjectiveVars (Bound a) Source # | |
| InjectiveVars a => InjectiveVars (Dom a) Source # | |
| InjectiveVars a => InjectiveVars (Measure a) Source # | |
| InjectiveVars a => InjectiveVars (Sort a) Source # | |
| InjectiveVars a => InjectiveVars (TBinding a) Source # | |
| InjectiveVars a => InjectiveVars (Tagged a) Source # | |
| InjectiveVars a => InjectiveVars (Maybe a) Source # | |
| InjectiveVars a => InjectiveVars [a] Source # | |
| (InjectiveVars a, InjectiveVars b) => InjectiveVars (a, b) Source # | |
| (InjectiveVars a, InjectiveVars b, InjectiveVars c) => InjectiveVars (a, b, c) Source # | |
isField :: FieldClass -> Bool Source #
isNamedField :: FieldInfo -> Bool Source #
destructorNames :: [FieldInfo] -> [Name] Source #
analyzeConstructor :: Co -> Name -> Telescope -> Constructor -> ConstructorInfo Source #
destructorNamesPresent :: [FieldInfo] -> Bool Source #
analyzeConstructors :: Co -> Name -> Telescope -> [Constructor] -> [ConstructorInfo] Source #
Analyze all constructors of a data type at once so that we can also check which constructors patterns are irrefutable.
reassembleConstructor :: ConstructorInfo -> Constructor Source #
Build constructor type from constructor info, erasing all indices.
reassembleConstructorType :: ConstructorInfo -> Type Source #
Assumes that all the indices (even from data telescope) are contained in fields.
exprToPattern :: Expr -> Maybe Pattern Source #
exprToPattern is used in the termination checker to convert
dot patterns into proper patterns.
patApp :: Pattern -> Pattern -> Maybe Pattern Source #
Only constructor patterns can be applied to a pattern.
exprToDotPat :: Expr -> (Bool, Pattern) Source #
exprToDotPat turns an expression into a pattern.
The Bool is True if the pattern is proper, i.e., does not contain
DotP except DotP Infty.
patternToExpr :: Pattern -> Expr Source #
dotConstructors :: Pattern -> Pattern Source #
Dot all constructor subpatterns. Used when expanding a dotted patsyn.
isDotPattern :: Pattern -> Bool Source #
isSuccessorPattern :: Pattern -> Bool Source #
isSuccessor :: Expr -> Bool Source #
shallowSuccP :: Pattern -> Bool Source #
typeToTele :: Type -> (Telescope, Type) Source #
typeToTele ((x : A) -> (y : B) -> C) = ([(x,A),(y,B)], C)
typeToTele' :: Int -> Type -> (Telescope, Type) Source #
typeToTele' k t.
If k > 0 it takes at most k leading Pis into the telescope
STALE: (hidden bindings do not count).
teleToTypeM :: Applicative m => (Dec -> m Dec) -> Telescope -> Type -> m Type Source #
adjustTopDecsM :: Applicative m => (Dec -> m Dec) -> Type -> m Type Source #