| Copyright | disco team and contributors |
|---|---|
| License | BSD-3-Clause |
| Maintainer | byorgey@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
Disco.AST.Surface
Description
Abstract syntax trees representing the surface syntax of the Disco language.
Synopsis
- data Module = Module {}
- data TopLevel
- type Docs = [DocThing]
- data DocThing
- type Property = Property_ UD
- data TypeDecl = TypeDecl (Name Term) PolyType
- data TermDefn = TermDefn (Name Term) [Bind [Pattern] Term]
- data TypeDefn = TypeDefn String [String] Type
- data Decl where
- partitionDecls :: [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
- prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc
- data UD
- type Term = Term_ UD
- pattern TVar :: Name Term -> Term
- pattern TPrim :: Prim -> Term
- pattern TUn :: UOp -> Term -> Term
- pattern TBin :: BOp -> Term -> Term -> Term
- pattern TLet :: Bind (Telescope Binding) Term -> Term
- pattern TParens :: Term -> Term
- pattern TUnit :: Term
- pattern TBool :: Bool -> Term
- pattern TChar :: Char -> Term
- pattern TString :: String -> Term
- pattern TNat :: Integer -> Term
- pattern TRat :: Rational -> Term
- pattern TAbs :: Quantifier -> Bind [Pattern] Term -> Term
- pattern TApp :: Term -> Term -> Term
- pattern TTup :: [Term] -> Term
- pattern TCase :: [Branch] -> Term
- pattern TChain :: Term -> [Link] -> Term
- pattern TTyOp :: TyOp -> Type -> Term
- pattern TContainerComp :: Container -> Bind (Telescope Qual) Term -> Term
- pattern TContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
- pattern TAscr :: Term -> PolyType -> Term
- pattern TWild :: Term
- pattern TList :: [Term] -> Maybe (Ellipsis Term) -> Term
- pattern TListComp :: Bind (Telescope Qual) Term -> Term
- data Quantifier
- data Telescope b where
- foldTelescope :: Alpha b => (b -> r -> r) -> r -> Telescope b -> r
- mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b
- toTelescope :: Alpha b => [b] -> Telescope b
- fromTelescope :: Alpha b => Telescope b -> [b]
- data Side
- type Link = Link_ UD
- pattern TLink :: BOp -> Term -> Link
- type Binding = Binding_ UD
- type Qual = Qual_ UD
- pattern QBind :: Name Term -> Embed Term -> Qual
- pattern QGuard :: Embed Term -> Qual
- data Container where
- data Ellipsis t where
- type Branch = Branch_ UD
- type Guard = Guard_ UD
- pattern GBool :: Embed Term -> Guard
- pattern GPat :: Embed Term -> Pattern -> Guard
- pattern GLet :: Binding -> Guard
- type Pattern = Pattern_ UD
- pattern PVar :: Name Term -> Pattern
- pattern PWild :: Pattern
- pattern PAscr :: Pattern -> Type -> Pattern
- pattern PUnit :: Pattern
- pattern PBool :: Bool -> Pattern
- pattern PChar :: Char -> Pattern
- pattern PString :: String -> Pattern
- pattern PTup :: [Pattern] -> Pattern
- pattern PInj :: Side -> Pattern -> Pattern
- pattern PNat :: Integer -> Pattern
- pattern PCons :: Pattern -> Pattern -> Pattern
- pattern PList :: [Pattern] -> Pattern
- pattern PAdd :: Side -> Pattern -> Term -> Pattern
- pattern PMul :: Side -> Pattern -> Term -> Pattern
- pattern PSub :: Pattern -> Term -> Pattern
- pattern PNeg :: Pattern -> Pattern
- pattern PFrac :: Pattern -> Pattern -> Pattern
- pattern Binding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
Modules
A module contains all the information from one disco source file.
Constructors
| Module | |
Documentation
An item of documentation.
Constructors
| DocString [String] | A documentation string, i.e. a block
of |
| DocProperty Property | An exampledoctestproperty of the
form |
type Property = Property_ UD Source #
A property is a universally quantified term of the form
forall v1 : T1, v2 : T2. term.
Declarations
A type declaration, name : type.
A group of definition clauses of the form name pat1 .. patn = term. The
patterns bind variables in the term. For example, f n (x,y) =
n*x + y.
A user-defined type (potentially recursive).
@type T arg1 arg2 ... = body
A declaration is either a type declaration, a term definition, or a type definition.
prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc Source #
Pretty-print a type declaration.
Terms
The extension descriptor for Surface specific AST types.
Instances
data Quantifier Source #
A quantifier: λ, ∀, or ∃
Instances
Telescopes
data Telescope b where Source #
A telescope is essentially a list, except that each item can bind names in the rest of the list.
Constructors
| TelEmpty :: Telescope b | The empty telescope. |
| TelCons :: Rebind b (Telescope b) -> Telescope b | A binder of type |
Instances
| Pretty Branch Source # | Pretty-print a single branch in a case expression. |
| HasType ABranch Source # | |
| Subst t b => Subst t (Telescope b) Source # | |
| Data b => Data (Telescope b) Source # | |
Defined in Disco.AST.Generic Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Telescope b -> c (Telescope b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Telescope b) # toConstr :: Telescope b -> Constr # dataTypeOf :: Telescope b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Telescope b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Telescope b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Telescope b -> Telescope b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Telescope b -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Telescope b -> r # gmapQ :: (forall d. Data d => d -> u) -> Telescope b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Telescope b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b) # | |
| Show b => Show (Telescope b) Source # | |
| Generic (Telescope b) Source # | |
| Alpha b => Alpha (Telescope b) Source # | |
Defined in Disco.AST.Generic Methods aeq' :: AlphaCtx -> Telescope b -> Telescope b -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b) # close :: AlphaCtx -> NamePatFind -> Telescope b -> Telescope b # open :: AlphaCtx -> NthPatFind -> Telescope b -> Telescope b # isPat :: Telescope b -> DisjointSet AnyName # isTerm :: Telescope b -> All # isEmbed :: Telescope b -> Bool # nthPatFind :: Telescope b -> NthPatFind # namePatFind :: Telescope b -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b # lfreshen' :: LFresh m => AlphaCtx -> Telescope b -> (Telescope b -> Perm AnyName -> m b0) -> m b0 # freshen' :: Fresh m => AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName) # acompare' :: AlphaCtx -> Telescope b -> Telescope b -> Ordering # | |
| Pretty (Telescope Guard) Source # | Pretty-print the guards in a single branch of a case expression. |
| Pretty (Telescope Qual) Source # | Pretty-print the qualifiers in a comprehension. |
| type Rep (Telescope b) Source # | |
Defined in Disco.AST.Generic type Rep (Telescope b) = D1 ('MetaData "Telescope" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "TelEmpty" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TelCons" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Rebind b (Telescope b))))) | |
foldTelescope :: Alpha b => (b -> r -> r) -> r -> Telescope b -> r Source #
Fold a telescope given a combining function and a value to use
for the empty telescope. Analogous to foldr for lists.
mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b Source #
Apply a function to every item in a telescope.
toTelescope :: Alpha b => [b] -> Telescope b Source #
Convert a list to a telescope.
fromTelescope :: Alpha b => Telescope b -> [b] Source #
Convert a telescope to a list.
Expressions
Injections into a sum type (inl or inr) have a "side" (L or R).
Instances
| Bounded Side Source # | |
| Enum Side Source # | |
| Eq Side Source # | |
| Data Side Source # | |
Defined in Disco.AST.Generic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Side -> c Side # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Side # dataTypeOf :: Side -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Side) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side) # gmapT :: (forall b. Data b => b -> b) -> Side -> Side # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r # gmapQ :: (forall d. Data d => d -> u) -> Side -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Side -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Side -> m Side # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Side -> m Side # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Side -> m Side # | |
| Ord Side Source # | |
| Show Side Source # | |
| Generic Side Source # | |
| Alpha Side Source # | |
Defined in Disco.AST.Generic Methods aeq' :: AlphaCtx -> Side -> Side -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side # close :: AlphaCtx -> NamePatFind -> Side -> Side # open :: AlphaCtx -> NthPatFind -> Side -> Side # isPat :: Side -> DisjointSet AnyName # nthPatFind :: Side -> NthPatFind # namePatFind :: Side -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Side -> Side # lfreshen' :: LFresh m => AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Side -> m (Side, Perm AnyName) # | |
| Pretty Side Source # | |
| Subst t Side Source # | |
| type Rep Side Source # | |
Lists
An enumeration of the different kinds of containers in disco: lists, bags, and sets.
Constructors
| ListContainer :: Container | |
| BagContainer :: Container | |
| SetContainer :: Container |
Instances
data Ellipsis t where Source #
An ellipsis is an "omitted" part of a literal container (such as
a list or set), of the form .. t. We don't have open-ended
ellipses since everything is evaluated eagerly and hence
containers must be finite.
Constructors
| Until :: t -> Ellipsis t |
|
Instances
| Functor Ellipsis Source # | |
| Foldable Ellipsis Source # | |
Defined in Disco.AST.Generic Methods fold :: Monoid m => Ellipsis m -> m # foldMap :: Monoid m => (a -> m) -> Ellipsis a -> m # foldMap' :: Monoid m => (a -> m) -> Ellipsis a -> m # foldr :: (a -> b -> b) -> b -> Ellipsis a -> b # foldr' :: (a -> b -> b) -> b -> Ellipsis a -> b # foldl :: (b -> a -> b) -> b -> Ellipsis a -> b # foldl' :: (b -> a -> b) -> b -> Ellipsis a -> b # foldr1 :: (a -> a -> a) -> Ellipsis a -> a # foldl1 :: (a -> a -> a) -> Ellipsis a -> a # elem :: Eq a => a -> Ellipsis a -> Bool # maximum :: Ord a => Ellipsis a -> a # minimum :: Ord a => Ellipsis a -> a # | |
| Traversable Ellipsis Source # | |
| Subst a t => Subst a (Ellipsis t) Source # | |
| Data t => Data (Ellipsis t) Source # | |
Defined in Disco.AST.Generic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ellipsis t) # toConstr :: Ellipsis t -> Constr # dataTypeOf :: Ellipsis t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Ellipsis t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Ellipsis t)) # gmapT :: (forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r # gmapQ :: (forall d. Data d => d -> u) -> Ellipsis t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t) # | |
| Show t => Show (Ellipsis t) Source # | |
| Generic (Ellipsis t) Source # | |
| Alpha t => Alpha (Ellipsis t) Source # | |
Defined in Disco.AST.Generic Methods aeq' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t) # close :: AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t # open :: AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t # isPat :: Ellipsis t -> DisjointSet AnyName # isEmbed :: Ellipsis t -> Bool # nthPatFind :: Ellipsis t -> NthPatFind # namePatFind :: Ellipsis t -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t # lfreshen' :: LFresh m => AlphaCtx -> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName) # acompare' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering # | |
| type Rep (Ellipsis t) Source # | |
Defined in Disco.AST.Generic | |