ermine-0.6: Ermine

Copyright(c) Edward Kmett and Dan Doel 2012
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable (DeriveDataTypeable)
Safe HaskellNone
LanguageHaskell2010

Ermine.Syntax.Term

Contents

Description

This module provides the AST for Terms

Synopsis

Terms

data Term t a Source

Terms in the Ermine language.

Constructors

Var a 
App !(Term t a) !(Term t a) 
HardTerm !HardTerm 
Sig !(Term t a) t 
Lam [Pattern t] !(Scope PatternPath (Term t) a) 
Case !(Term t a) [Alt t (Term t) a] 
Let [Binding t a] !(Scope Word64 (Term t) a) 
Loc !Rendering !(Term t a)

informational link to the location the term came from

Remember !Int !(Term t a)

Used to provide hole support.

Instances

Show2 Term 
Eq2 Term 
Bitraversable Term 
Serial2 Term 
Bifunctor Term 
Bifoldable Term 
((~) (* -> * -> *) p (Tagged *), (~) (* -> *) f Identity) => Tup p f (Term t a) 
Monad (Term t) 
Functor (Term t) 
Applicative (Term t) 
Foldable (Term t) 
Traversable (Term t) 
Show t => Show1 (Term t) 
Eq t => Eq1 (Term t) 
Serial t => Serial1 (Term t) 
App (Term t) 
Variable (Term t) 
(Eq t, Eq a) => Eq (Term t a) 
(Show t, Show a) => Show (Term t a) 
IsString a => IsString (Term t a) 
(Binary t, Binary v) => Binary (Term t v) 
(Serialize t, Serialize v) => Serialize (Term t v) 
(Serial t, Serial v) => Serial (Term t v) 
Terminal (Term t a) 
HasKindVars t t' k k' => HasKindVars (Term t a) (Term t' a) k k' 
HasTypeVars t t' tv tv' => HasTypeVars (Term t a) (Term t' a) tv tv' 

bindTerm :: (t -> t') -> (a -> Term t' b) -> Term t a -> Term t' b Source

Perform simultaneous substitution on terms and type annotations.

Hard Terms

data HardTerm Source

Simple terms that can be compared with structural equality.

Constructors

Lit Literal 
DataCon !Global (Type Void Void) 
Tuple !Word64 
Hole

A placeholder that can take any type. Easy to Remember.

Instances

class Terminal t where Source

This class provides a prism to match against or inject a HardTerm.

Minimal complete definition

hardTerm

Methods

hardTerm :: Prism' t HardTerm Source

litTerm :: Literal -> t Source

hole :: t Source

Instances

Bindings

data BodyBound Source

Bound variables in a declaration are rather complicated. One can refer to any of the following: 1. Definitions in the same declaration sequence 2. Variables bound in a pattern 3. Definitions in a where clause the DeclBound type captures these three cases in the respective constructors.

Constructors

BodyDecl Word64 
BodyPat PatternPath 
BodyWhere Word64 

Instances

data WhereBound Source

Constructors

WhereDecl Word64 
WherePat PatternPath 

Instances

class AsDecl t where Source

Minimal complete definition

Nothing

Methods

_Decl :: Prism' t Word64 Source

Instances

data Binding t a Source

A Binding provides its source location as a rendering, knowledge of if it is explicit or implicitly bound and a list of right hand side bindings.

Constructors

Binding 

Fields

_bindingLoc :: !Rendering
 
_bindingType :: !(BindingType t)
 
_bindingBodies :: [Body t a]
 

Instances

Bitraversable Binding 
Serial2 Binding 
Bifunctor Binding 
Bifoldable Binding 
Functor (Binding t) 
Foldable (Binding t) 
Traversable (Binding t) 
Serial t => Serial1 (Binding t) 
(Eq t, Eq a) => Eq (Binding t a) 
(Show t, Show a) => Show (Binding t a) 
(Binary t, Binary v) => Binary (Binding t v) 
(Serial t, Serial v) => Serial (Binding t v) 
HasBinding (Binding t a) t a 

class HasBinding t t a | t -> t a where Source

Minimal complete definition

binding

Methods

binding :: Lens' t (Binding t a) Source

bindingBodies :: Lens' t [Body t a] Source

bindingLoc :: Lens' t Rendering Source

bindingType :: Lens' t (BindingType t) Source

Instances

HasBinding (Binding t a) t a 

data BindingType t Source

Indicate if a definition is explicitly bound with a type annotation or implicitly bound without.

Constructors

Explicit t 
Implicit 

Instances

Functor BindingType 
Foldable BindingType 
Traversable BindingType 
Serial1 BindingType 
Eq t => Eq (BindingType t) 
Show t => Show (BindingType t) 
Generic (BindingType t) 
Binary t => Binary (BindingType t) 
Serialize t => Serialize (BindingType t) 
Serial t => Serial (BindingType t) 
type Rep (BindingType t) 

_Implicit :: forall t. Prism' (BindingType t) () Source

_Explicit :: forall t t. Prism (BindingType t) (BindingType t) t t Source

data Body t a Source

A body is the right hand side of a definition. This isn't a term because it has to perform simultaneous matches on multiple patterns with backtracking. Each Body contains a list of where clause bindings to which the body and guards can refer.

Constructors

Body 

Fields

_bodyPatterns :: [Pattern t]
 
_bodyGuarded :: Guarded (Scope BodyBound (Term t) a)
 
_bodyWhere :: [Binding t (Var WhereBound a)]
 

Instances

Bitraversable Body 
Serial2 Body 
Bifunctor Body 
Bifoldable Body 
Functor (Body t) 
Foldable (Body t) 
Traversable (Body t) 
Serial t => Serial1 (Body t) 
(Eq t, Eq a) => Eq (Body t a) 
(Show t, Show a) => Show (Body t a) 
(Binary t, Binary a) => Binary (Body t a) 
(Serialize t, Serialize a) => Serialize (Body t a) 
(Serial t, Serial v) => Serial (Body t v) 

bodyPatterns :: forall t a. Lens' (Body t a) [Pattern t] Source

bodyGuarded :: forall t a. Lens' (Body t a) (Guarded (Scope BodyBound (Term t) a)) Source

bodyWhere :: forall t a. Lens' (Body t a) [Binding t (Var WhereBound a)] Source

bodyDecls :: Traversal' (Body t a) Word64 Source