Safe Haskell	None
Language	Haskell98

DDC.Source.Tetra.Exp.Source

Contents

Language
Binding
Types
- Syntax
- Primitives
Terms

Synopsis

Language

data Source Source #

Type index for Source Tetra Language.

Constructors

Source

Instances

Show Source Source #
Methods showsPrec :: Int -> Source -> ShowS # show :: Source -> String # showList :: [Source] -> ShowS #
Pretty Source Source #
Associated Types data PrettyMode Source :: * # Methods pprDefaultMode :: PrettyMode Source # ppr :: Source -> Doc # pprPrec :: Int -> Source -> Doc # pprModePrec :: PrettyMode Source -> Int -> Source -> Doc #
Anon Source Source #
Methods withBinding :: Source -> (GTBindVar Source -> GTBoundVar Source -> a) -> a # withBindings :: Source -> Int -> ([GTBindVar Source] -> [GTBoundVar Source] -> a) -> a #
HasAnonBind Source Source #
Methods isAnon :: Source -> GXBindVar Source -> Bool Source #
Expand AltMatch Source #
Methods expand :: SourcePos -> Env -> AltMatch -> AltMatch Source #
Expand AltCase Source #
Methods expand :: SourcePos -> Env -> AltCase -> AltCase Source #
Expand GuardedExp Source #
Methods expand :: SourcePos -> Env -> GuardedExp -> GuardedExp Source #
Expand Guard Source #
Methods expand :: SourcePos -> Env -> Guard -> Guard Source #
Expand Clause Source #
Methods expand :: SourcePos -> Env -> Clause -> Clause Source #
Expand Exp Source #
Methods expand :: SourcePos -> Env -> Exp -> Exp Source #
Expand (Top Source) Source #
Methods expand :: SourcePos -> Env -> Top Source -> Top Source Source #
Expand (Module Source) Source #
Methods expand :: SourcePos -> Env -> Module Source -> Module Source Source #
type GTAnnot Source Source #
type GTAnnot Source = SourcePos
type GTBindVar Source Source #
type GTBindVar Source = Bind
type GTBoundVar Source Source #
type GTBoundVar Source = Bound
type GTBindCon Source Source #
type GTBindCon Source = TyConBind
type GTBoundCon Source Source #
type GTBoundCon Source = TyConBound
type GTPrim Source Source #
type GTPrim Source = PrimType
type GXPrim Source Source #
type GXPrim Source = PrimVal
type GXBoundCon Source Source #
type GXBoundCon Source = DaConBound
type GXBindCon Source Source #
type GXBindCon Source = DaConBind
type GXBoundVar Source Source #
type GXBoundVar Source = Bound
type GXBindVar Source Source #
type GXBindVar Source = Bind
type GXAnnot Source Source #
type GXAnnot Source = SourcePos

Binding

type Name = Text Source #

data Bind Source #

Binding occurrence of a variable.

Constructors

BNone
BAnon
BName !Text

Instances

Eq Bind Source #
Methods (==) :: Bind -> Bind -> Bool # (/=) :: Bind -> Bind -> Bool #
Ord Bind Source #
Methods compare :: Bind -> Bind -> Ordering # (<) :: Bind -> Bind -> Bool # (<=) :: Bind -> Bind -> Bool # (>) :: Bind -> Bind -> Bool # (>=) :: Bind -> Bind -> Bool # max :: Bind -> Bind -> Bind # min :: Bind -> Bind -> Bind #
Show Bind Source #
Methods showsPrec :: Int -> Bind -> ShowS # show :: Bind -> String # showList :: [Bind] -> ShowS #

data Bound Source #

Bound occurrence of a variable.

Constructors

UName !Text
UIx !Int
UHole

Instances

Eq Bound Source #
Methods (==) :: Bound -> Bound -> Bool # (/=) :: Bound -> Bound -> Bool #
Ord Bound Source #
Methods compare :: Bound -> Bound -> Ordering # (<) :: Bound -> Bound -> Bool # (<=) :: Bound -> Bound -> Bool # (>) :: Bound -> Bound -> Bool # (>=) :: Bound -> Bound -> Bool # max :: Bound -> Bound -> Bound # min :: Bound -> Bound -> Bound #
Show Bound Source #
Methods showsPrec :: Int -> Bound -> ShowS # show :: Bound -> String # showList :: [Bound] -> ShowS #

Types

Syntax

type family GTAnnot l :: * #

Yield the type of annotations.

Instances

type GTAnnot Source #
type GTAnnot Source = SourcePos

type family GTBindVar l :: * #

Yield the type of binding occurrences of variables.

Instances

type GTBindVar Source #
type GTBindVar Source = Bind

type family GTBoundVar l :: * #

Yield the type of bound occurrences of variables.

Instances

type GTBoundVar Source #
type GTBoundVar Source = Bound

type family GTBindCon l :: * #

Yield the type of binding occurrences of constructors.

Instances

type GTBindCon Source #
type GTBindCon Source = TyConBind

type family GTBoundCon l :: * #

Yield the type of bound occurrences of constructors.

Instances

type GTBoundCon Source #
type GTBoundCon Source = TyConBound

type family GTPrim l :: * #

Yield the type of primitive type names.

Instances

type GTPrim Source #
type GTPrim Source = PrimType

type Type = GType Source Source #

data GType l :: * -> * #

Generic type expression representation.

Constructors

TAnnot ~(GTAnnot l) (GType l)	An annotated type.
TCon ~(GTyCon l)	Type constructor or literal.
TVar ~(GTBoundVar l)	Type variable.
TAbs ~(GTBindVar l) (GType l) (GType l)	Type abstracton.
TApp ~(GType l) (GType l)	Type application.

Instances

(Eq (GTAnnot l), Eq (GTyCon l), Eq (GTBindVar l), Eq (GTBoundVar l)) => Eq (GType l)
Methods (==) :: GType l -> GType l -> Bool # (/=) :: GType l -> GType l -> Bool #
ShowGType l => Show (GType l)
Methods showsPrec :: Int -> GType l -> ShowS # show :: GType l -> String # showList :: [GType l] -> ShowS #

type TyCon = GTyCon Source Source #

data GTyCon l :: * -> * #

Wrapper for primitive constructors that adds the ones common to SystemFω based languages.

Constructors

TyConVoid	The void constructor.
TyConUnit	The unit constructor.
TyConFun	The function constructor.
TyConUnion ~(GType l)	Take the least upper bound at the given kind.
TyConBot ~(GType l)	The least element of the given kind.
TyConForall ~(GType l)	The universal quantifier with a parameter of the given kind.
TyConExists ~(GType l)	The existential quantifier with a parameter of the given kind.
TyConPrim ~(GTPrim l)	Primitive constructor.
TyConBound ~(GTBoundCon l)	Bound constructor.

Instances

(Eq (GType l), Eq (GTPrim l), Eq (GTBoundCon l)) => Eq (GTyCon l)
Methods (==) :: GTyCon l -> GTyCon l -> Bool # (/=) :: GTyCon l -> GTyCon l -> Bool #
ShowGType l => Show (GTyCon l)
Methods showsPrec :: Int -> GTyCon l -> ShowS # show :: GTyCon l -> String # showList :: [GTyCon l] -> ShowS #

data SoCon :: * #

Sort constructor.

Constructors

SoConProp	Sort of witness kinds.
SoConComp	Sort of computation kinds.

Instances

Eq SoCon
Methods (==) :: SoCon -> SoCon -> Bool # (/=) :: SoCon -> SoCon -> Bool #
Ord SoCon
Methods compare :: SoCon -> SoCon -> Ordering # (<) :: SoCon -> SoCon -> Bool # (<=) :: SoCon -> SoCon -> Bool # (>) :: SoCon -> SoCon -> Bool # (>=) :: SoCon -> SoCon -> Bool # max :: SoCon -> SoCon -> SoCon # min :: SoCon -> SoCon -> SoCon #
Show SoCon
Methods showsPrec :: Int -> SoCon -> ShowS # show :: SoCon -> String # showList :: [SoCon] -> ShowS #

data KiCon :: * #

Kind constructor.

Constructors

KiConFun	Function kind constructor. This is only well formed when it is fully applied.
KiConWitness	Kind of witnesses.
KiConData	Kind of data values.
KiConRegion	Kind of regions.
KiConEffect	Kind of effects.
KiConClosure	Kind of closures.

Instances

Eq KiCon
Methods (==) :: KiCon -> KiCon -> Bool # (/=) :: KiCon -> KiCon -> Bool #
Ord KiCon
Methods compare :: KiCon -> KiCon -> Ordering # (<) :: KiCon -> KiCon -> Bool # (<=) :: KiCon -> KiCon -> Bool # (>) :: KiCon -> KiCon -> Bool # (>=) :: KiCon -> KiCon -> Bool # max :: KiCon -> KiCon -> KiCon # min :: KiCon -> KiCon -> KiCon #
Show KiCon
Methods showsPrec :: Int -> KiCon -> ShowS # show :: KiCon -> String # showList :: [KiCon] -> ShowS #

data TwCon :: * #

Witness type constructors.

Constructors

TwConImpl
TwConPure	Purity of some effect.
TwConConst	Constancy of some region.
TwConDeepConst	Constancy of material regions in some type
TwConMutable	Mutability of some region.
TwConDeepMutable	Mutability of material regions in some type.
TwConDistinct Int	Distinctness of some n regions
TwConDisjoint	Non-interfering effects are disjoint. Used for rewrite rules.

Instances

Eq TwCon
Methods (==) :: TwCon -> TwCon -> Bool # (/=) :: TwCon -> TwCon -> Bool #
Ord TwCon
Methods compare :: TwCon -> TwCon -> Ordering # (<) :: TwCon -> TwCon -> Bool # (<=) :: TwCon -> TwCon -> Bool # (>) :: TwCon -> TwCon -> Bool # (>=) :: TwCon -> TwCon -> Bool # max :: TwCon -> TwCon -> TwCon # min :: TwCon -> TwCon -> TwCon #
Show TwCon
Methods showsPrec :: Int -> TwCon -> ShowS # show :: TwCon -> String # showList :: [TwCon] -> ShowS #

data TcCon :: * #

Other constructors at the spec level.

Constructors

TcConUnit	The unit data type constructor is baked in.
TcConFun	Pure function.
TcConSusp	A suspended computation.
TcConRead	Read of some region.
TcConHeadRead	Read the head region in a data type.
TcConDeepRead	Read of all material regions in a data type.
TcConWrite	Write of some region.
TcConDeepWrite	Write to all material regions in some data type.
TcConAlloc	Allocation into some region.
TcConDeepAlloc	Allocation into all material regions in some data type.

Instances

Eq TcCon
Methods (==) :: TcCon -> TcCon -> Bool # (/=) :: TcCon -> TcCon -> Bool #
Ord TcCon
Methods compare :: TcCon -> TcCon -> Ordering # (<) :: TcCon -> TcCon -> Bool # (<=) :: TcCon -> TcCon -> Bool # (>) :: TcCon -> TcCon -> Bool # (>=) :: TcCon -> TcCon -> Bool # max :: TcCon -> TcCon -> TcCon # min :: TcCon -> TcCon -> TcCon #
Show TcCon
Methods showsPrec :: Int -> TcCon -> ShowS # show :: TcCon -> String # showList :: [TcCon] -> ShowS #

data TyConBind Source #

Binding occurrence of a type constructor.

Constructors

TyConBindName Text

Instances

Eq TyConBind Source #
Methods (==) :: TyConBind -> TyConBind -> Bool # (/=) :: TyConBind -> TyConBind -> Bool #
Ord TyConBind Source #
Methods compare :: TyConBind -> TyConBind -> Ordering # (<) :: TyConBind -> TyConBind -> Bool # (<=) :: TyConBind -> TyConBind -> Bool # (>) :: TyConBind -> TyConBind -> Bool # (>=) :: TyConBind -> TyConBind -> Bool # max :: TyConBind -> TyConBind -> TyConBind # min :: TyConBind -> TyConBind -> TyConBind #
Show TyConBind Source #
Methods showsPrec :: Int -> TyConBind -> ShowS # show :: TyConBind -> String # showList :: [TyConBind] -> ShowS #

data TyConBound Source #

Bound occurrence of a type constructor.

Constructors

TyConBoundName Text

Instances

Eq TyConBound Source #
Methods (==) :: TyConBound -> TyConBound -> Bool # (/=) :: TyConBound -> TyConBound -> Bool #
Ord TyConBound Source #
Methods compare :: TyConBound -> TyConBound -> Ordering # (<) :: TyConBound -> TyConBound -> Bool # (<=) :: TyConBound -> TyConBound -> Bool # (>) :: TyConBound -> TyConBound -> Bool # (>=) :: TyConBound -> TyConBound -> Bool # max :: TyConBound -> TyConBound -> TyConBound # min :: TyConBound -> TyConBound -> TyConBound #
Show TyConBound Source #
Methods showsPrec :: Int -> TyConBound -> ShowS # show :: TyConBound -> String # showList :: [TyConBound] -> ShowS #

pattern TApp2 :: forall t. GType t -> GType t -> GType t -> GType t #

Applcation of a type to two arguments.

pattern TApp3 :: forall t. GType t -> GType t -> GType t -> GType t -> GType t #

Applcation of a type to three arguments.

pattern TApp4 :: forall t. GType t -> GType t -> GType t -> GType t -> GType t -> GType t #

Applcation of a type to four arguments.

pattern TApp5 :: forall t. GType t -> GType t -> GType t -> GType t -> GType t -> GType t -> GType t #

Applcation of a type to five arguments.

pattern TVoid :: forall t. GType t #

Representation of the void type.

pattern TUnit :: forall t. GType t #

Representation of the unit type.

pattern TFun :: forall t. GType t -> GType t -> GType t #

Representation of the function type.

pattern TBot :: forall t. GType t -> GType t #

Representation of the bottom type at a given kind.

pattern TUnion :: forall t. GType t -> GType t -> GType t -> GType t #

Representation of a union of two types.

pattern TPrim :: forall t. GTPrim t -> GType t #

Representation of primitive type constructors.

Primitives

data PrimType Source #

Primitive types.

Constructors

PrimTypeSoCon !SoCon	Primitive sort constructors.
PrimTypeKiCon !KiCon	Primitive kind constructors.
PrimTypeTwCon !TwCon	Primitive witness type constructors.
PrimTypeTcCon !TcCon	Other type constructors at the spec level.
PrimTypeTyCon !PrimTyCon	Primitive machine type constructors.
PrimTypeTyConTetra !PrimTyConTetra	Primtiive type constructors specific to the Tetra fragment.

Instances

Eq PrimType Source #
Methods (==) :: PrimType -> PrimType -> Bool # (/=) :: PrimType -> PrimType -> Bool #
Ord PrimType Source #
Methods compare :: PrimType -> PrimType -> Ordering # (<) :: PrimType -> PrimType -> Bool # (<=) :: PrimType -> PrimType -> Bool # (>) :: PrimType -> PrimType -> Bool # (>=) :: PrimType -> PrimType -> Bool # max :: PrimType -> PrimType -> PrimType # min :: PrimType -> PrimType -> PrimType #
Show PrimType Source #
Methods showsPrec :: Int -> PrimType -> ShowS # show :: PrimType -> String # showList :: [PrimType] -> ShowS #

data PrimTyCon :: * #

Primitive type constructors.

Constructors

PrimTyConVoid	`Void#` the Void type has no values.
PrimTyConBool	`Bool#` unboxed booleans.
PrimTyConNat	`Nat#` natural numbers. Enough precision to count every object in the heap, but NOT necessearily enough precision to count every byte of memory.
PrimTyConInt	`Int#` signed integers. Enough precision to count every object in the heap, but NOT necessearily enough precision to count every byte of memory. If N is the total number of objects that can exist in the heap, then the range of `Int#` is at least (-N .. +N) inclusive.
PrimTyConSize	`Size#` unsigned sizes. Enough precision to count every addressable bytes of memory.
PrimTyConWord Int	`WordN#` machine words of the given width.
PrimTyConFloat Int	`FloatN#` floating point numbers of the given width.
PrimTyConVec Int	`VecN#` a packed vector of N values. This is intended to have kind (Data -> Data), so we use concrete vector types like `Vec4`.
PrimTyConAddr	`Addr#` a relative or absolute machine address. Enough precision to count every byte of memory. Unlike pointers below, an absolute `Addr#` need not refer to memory owned by the current process.
PrimTyConPtr	`Ptr#` like `Addr#`, but with a region and element type annotation. In particular, a value of a type like (Ptr) must be at least 4-byte aligned and point to memory owned by the current process.
PrimTyConTextLit	`TextLit#` type of a text literal, which is represented as a pointer to the literal data in static memory.
PrimTyConTag	`Tag#` data constructor tags. Enough precision to count every possible alternative of an enumerated type.

Instances

Eq PrimTyCon
Methods (==) :: PrimTyCon -> PrimTyCon -> Bool # (/=) :: PrimTyCon -> PrimTyCon -> Bool #
Ord PrimTyCon
Methods compare :: PrimTyCon -> PrimTyCon -> Ordering # (<) :: PrimTyCon -> PrimTyCon -> Bool # (<=) :: PrimTyCon -> PrimTyCon -> Bool # (>) :: PrimTyCon -> PrimTyCon -> Bool # (>=) :: PrimTyCon -> PrimTyCon -> Bool # max :: PrimTyCon -> PrimTyCon -> PrimTyCon # min :: PrimTyCon -> PrimTyCon -> PrimTyCon #
Show PrimTyCon
Methods showsPrec :: Int -> PrimTyCon -> ShowS # show :: PrimTyCon -> String # showList :: [PrimTyCon] -> ShowS #
Pretty PrimTyCon
Associated Types data PrettyMode PrimTyCon :: * # Methods pprDefaultMode :: PrettyMode PrimTyCon # ppr :: PrimTyCon -> Doc # pprPrec :: Int -> PrimTyCon -> Doc # pprModePrec :: PrettyMode PrimTyCon -> Int -> PrimTyCon -> Doc #
NFData PrimTyCon
Methods rnf :: PrimTyCon -> () #

data PrimTyConTetra Source #

Primitive type constructors specific to the Tetra language fragment.

Constructors

PrimTyConTetraTuple !Int	`TupleN#`. Tuples.
PrimTyConTetraVector	`Vector#`. Vectors.
PrimTyConTetraF	`F#`. Reified function values.
PrimTyConTetraC	`C#`. Reified function closures.
PrimTyConTetraU	`U#`. Explicitly unboxed values.

Instances

Eq PrimTyConTetra Source #
Methods (==) :: PrimTyConTetra -> PrimTyConTetra -> Bool # (/=) :: PrimTyConTetra -> PrimTyConTetra -> Bool #
Ord PrimTyConTetra Source #
Methods compare :: PrimTyConTetra -> PrimTyConTetra -> Ordering # (<) :: PrimTyConTetra -> PrimTyConTetra -> Bool # (<=) :: PrimTyConTetra -> PrimTyConTetra -> Bool # (>) :: PrimTyConTetra -> PrimTyConTetra -> Bool # (>=) :: PrimTyConTetra -> PrimTyConTetra -> Bool # max :: PrimTyConTetra -> PrimTyConTetra -> PrimTyConTetra # min :: PrimTyConTetra -> PrimTyConTetra -> PrimTyConTetra #
Show PrimTyConTetra Source #
Methods showsPrec :: Int -> PrimTyConTetra -> ShowS # show :: PrimTyConTetra -> String # showList :: [PrimTyConTetra] -> ShowS #

pattern KData :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Representation of the Data kind.

pattern KRegion :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Representation of the Region kind.

pattern KEffect :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Representation of the Effect kind.

pattern TImpl :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t Source #

Representation of an implication type.

pattern TSusp :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t Source #

Representation of a suspension type.

pattern TRead :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t Source #

Representation of a read effect.

pattern TWrite :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t Source #

Representation of a write effect.

pattern TAlloc :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t Source #

Representation of a alloc effect.

pattern TBool :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Primitive Bool type.

pattern TNat :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Primitive Nat type.

pattern TInt :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Primitive Int type.

pattern TSize :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Primitive Size type.

pattern TWord :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t Source #

Primitive WordN type of the given width.

pattern TFloat :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t Source #

Primitive FloatN type of the given width.

pattern TTextLit :: forall t. (~#) * * (GTPrim t) PrimType => GType t Source #

Primitive TextLit type.

Terms

Syntax

type Annot = GXAnnot Source Source #

type family GXAnnot l Source #

Yield the type of annotations.

Instances

type GXAnnot Source Source #
type GXAnnot Source = SourcePos

type BindVarMT = GXBindVarMT Source Source #

data GXBindVarMT l Source #

A possibly typed binding.

Constructors

XBindVarMT (GXBindVar l) (Maybe (GType l))

Instances

ShowLanguage l => Show (GXBindVarMT l) Source #
Methods showsPrec :: Int -> GXBindVarMT l -> ShowS # show :: GXBindVarMT l -> String # showList :: [GXBindVarMT l] -> ShowS #

type BindVar = GXBindVar Source Source #

type family GXBindVar l Source #

Yield the type of binding occurrences of variables.

Instances

type GXBindVar Source Source #
type GXBindVar Source = Bind

type BoundVar = GXBoundVar Source Source #

type family GXBoundVar l Source #

Yield the type of bound occurrences of variables.

Instances

type GXBoundVar Source Source #
type GXBoundVar Source = Bound

type BindCon = GXBoundCon Source Source #

type family GXBindCon l Source #

Yield the type of binding occurrences of constructors.

Instances

type GXBindCon Source Source #
type GXBindCon Source = DaConBind

type BoundCon = GXBoundCon Source Source #

type family GXBoundCon l Source #

Yield the type of bound occurrences of constructors.

Instances

type GXBoundCon Source Source #
type GXBoundCon Source = DaConBound

type Prim = GXPrim Source Source #

type family GXPrim l Source #

Yield the type of primitive operator names.

Instances

type GXPrim Source Source #
type GXPrim Source = PrimVal

type Exp = GExp Source Source #

data GExp l Source #

Well-typed expressions have types of kind Data.

Constructors

XAnnot !(GXAnnot l) !(GExp l)
XVar !(GXBoundVar l)	Value variable or primitive operation.
XPrim !(GXPrim l)	Primitive values.
XCon !(DaCon (GXBoundCon l) (GType l))	Data constructor or literal.
XLAM !(GXBindVarMT l) !(GExp l)	Type abstraction (level-1).
XLam !(GXBindVarMT l) !(GExp l)	Value and Witness abstraction (level-0).
XApp !(GExp l) !(GExp l)	Application.
XLet !(GLets l) !(GExp l)	A non-recursive let-binding.
XCase !(GExp l) ![GAltCase l]	Case branching.
XCast !(GCast l) !(GExp l)	Type cast.
XType !(GType l)	Type can appear as the argument of an application.
XWitness !(GWitness l)	Witness can appear as the argument of an application.
XDefix !(GXAnnot l) [GExp l]	Some expressions and infix operators that need to be resolved into proper function applications.
XInfixOp !(GXAnnot l) String	Use of a naked infix operator, like in 1 + 2. INVARIANT: only appears in the list of an XDefix node.
XInfixVar !(GXAnnot l) String	Use of an infix operator as a plain variable, like in (+) 1 2. INVARIANT: only appears in the list of an XDefix node.
XMatch !(GXAnnot l) ![GAltMatch l] !(GExp l)	Match expression with default. Similar to a case expression, except that if an alternative fails then we try the next one instead of failing. If none of the alternatives succeeds then the overall value is the value of the default expression.
XWhere !(GXAnnot l) !(GExp l) ![GClause l]	Where expression defines a group of recursive clauses, and is desugared to a letrec.
XLamPat !(GXAnnot l) !(GPat l) !(Maybe (GType l)) !(GExp l)	Lambda abstraction which matches its argument against a single pattern.
XLamCase !(GXAnnot l) ![GAltCase l]	Lambda abstraction that matches its argument against the given alternatives.

Instances

Expand Exp Source #
Methods expand :: SourcePos -> Env -> Exp -> Exp Source #
HasAnonBind l => MapBoundX GExp l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GExp l -> GExp l Source #
Defix GExp l Source #
Methods defix :: FixTable l -> GExp l -> Either (Error l) (GExp l) Source #
ShowLanguage l => Show (GExp l) Source #
Methods showsPrec :: Int -> GExp l -> ShowS # show :: GExp l -> String # showList :: [GExp l] -> ShowS #

type Lets = GLets Source Source #

data GLets l Source #

Possibly recursive bindings. Whether these are taken as recursive depends on whether they appear in an XLet or XLetrec group.

Constructors

LLet !(GXBindVarMT l) !(GExp l)	Non-recursive expression binding.
LRec ![(GXBindVarMT l, GExp l)]	Recursive binding of lambda abstractions.
LPrivate ![GXBindVar l] !(Maybe (GType l)) ![(GXBindVar l, GType l)]	Bind a local region variable, and witnesses to its properties.
LGroup ![GClause l]	A possibly recursive group of binding clauses. Multiple clauses in the group may be part of the same function.

Instances

Defix GLets l Source #
Methods defix :: FixTable l -> GLets l -> Either (Error l) (GLets l) Source #
ShowLanguage l => Show (GLets l) Source #
Methods showsPrec :: Int -> GLets l -> ShowS # show :: GLets l -> String # showList :: [GLets l] -> ShowS #

type Clause = GClause Source Source #

data GClause l Source #

Binding clause

Constructors

SSig !(GXAnnot l) !(GXBindVar l) !(GType l)	A separate type signature.
SLet !(GXAnnot l) !(GXBindVarMT l) ![GParam l] ![GGuardedExp l]	A function binding using pattern matching and guards.

Instances

Expand Clause Source #
Methods expand :: SourcePos -> Env -> Clause -> Clause Source #
HasAnonBind l => MapBoundX GClause l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GClause l -> GClause l Source #
Defix GClause l Source #
Methods defix :: FixTable l -> GClause l -> Either (Error l) (GClause l) Source #
ShowLanguage l => Show (GClause l) Source #
Methods showsPrec :: Int -> GClause l -> ShowS # show :: GClause l -> String # showList :: [GClause l] -> ShowS #

type Param = GParam Source Source #

data GParam l Source #

Parameter for a binding.

Constructors

MType !(GXBindVar l) (Maybe (GType l))	Type parameter with optional kind.
MWitness !(GXBindVar l) (Maybe (GType l))	Witness parameter with optional type.
MValue !(GPat l) (Maybe (GType l))	Value paatter with optional type.

Instances

ShowLanguage l => Show (GParam l) Source #
Methods showsPrec :: Int -> GParam l -> ShowS # show :: GParam l -> String # showList :: [GParam l] -> ShowS #

type Pat = GPat Source Source #

data GPat l Source #

Patterns.

Constructors

PDefault	The default pattern always succeeds.
PAt !(GXBindVar l) !(GPat l)	Give a name to the value matched by a pattern.
PVar !(GXBindVar l)	The variable pattern always succeeds and binds the value to the new variable.
PData !(DaCon (GXBoundCon l) (GType l)) ![GPat l]	Match a data constructor and bind its arguments.

Instances

ShowLanguage l => Show (GPat l) Source #
Methods showsPrec :: Int -> GPat l -> ShowS # show :: GPat l -> String # showList :: [GPat l] -> ShowS #

type Guard = GGuard Source Source #

data GGuard l Source #

Expression guards.

Constructors

GPat !(GPat l) !(GExp l)
GPred !(GExp l)
GDefault

Instances

Expand Guard Source #
Methods expand :: SourcePos -> Env -> Guard -> Guard Source #
HasAnonBind l => MapBoundX GGuard l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GGuard l -> GGuard l Source #
Defix GGuard l Source #
Methods defix :: FixTable l -> GGuard l -> Either (Error l) (GGuard l) Source #
ShowLanguage l => Show (GGuard l) Source #
Methods showsPrec :: Int -> GGuard l -> ShowS # show :: GGuard l -> String # showList :: [GGuard l] -> ShowS #

type GuardedExp = GGuardedExp Source Source #

data GGuardedExp l Source #

An expression with some guards.

Constructors

GGuard !(GGuard l) !(GGuardedExp l)
GExp !(GExp l)

Instances

Expand GuardedExp Source #
Methods expand :: SourcePos -> Env -> GuardedExp -> GuardedExp Source #
HasAnonBind l => MapBoundX GGuardedExp l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GGuardedExp l -> GGuardedExp l Source #
Defix GGuardedExp l Source #
Methods defix :: FixTable l -> GGuardedExp l -> Either (Error l) (GGuardedExp l) Source #
ShowLanguage l => Show (GGuardedExp l) Source #
Methods showsPrec :: Int -> GGuardedExp l -> ShowS # show :: GGuardedExp l -> String # showList :: [GGuardedExp l] -> ShowS #

type AltMatch = GAltMatch Source Source #

data GAltMatch l Source #

Match alternative. This is like a case alternative except that the match expression does not give us a head pattern.

Constructors

AAltMatch !(GGuardedExp l)

Instances

Expand AltMatch Source #
Methods expand :: SourcePos -> Env -> AltMatch -> AltMatch Source #
HasAnonBind l => MapBoundX GAltMatch l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GAltMatch l -> GAltMatch l Source #
Defix GAltMatch l Source #
Methods defix :: FixTable l -> GAltMatch l -> Either (Error l) (GAltMatch l) Source #
ShowLanguage l => Show (GAltMatch l) Source #
Methods showsPrec :: Int -> GAltMatch l -> ShowS # show :: GAltMatch l -> String # showList :: [GAltMatch l] -> ShowS #

type AltCase = GAltCase Source Source #

data GAltCase l Source #

Case alternative. If the pattern matches then bind the variables then enter the guarded expression.

Constructors

AAltCase !(GPat l) ![GGuardedExp l]

Instances

Expand AltCase Source #
Methods expand :: SourcePos -> Env -> AltCase -> AltCase Source #
HasAnonBind l => MapBoundX GAltCase l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GAltCase l -> GAltCase l Source #
Defix GAltCase l Source #
Methods defix :: FixTable l -> GAltCase l -> Either (Error l) (GAltCase l) Source #
ShowLanguage l => Show (GAltCase l) Source #
Methods showsPrec :: Int -> GAltCase l -> ShowS # show :: GAltCase l -> String # showList :: [GAltCase l] -> ShowS #

type Cast = GCast Source Source #

data GCast l Source #

Type casts.

Constructors

CastWeakenEffect !(GType l)	Weaken the effect of an expression. The given effect is added to the effect of the body.
CastPurify !(GWitness l)	Purify the effect (action) of an expression.
CastBox	Box a computation, capturing its effects in the S computation type.
CastRun	Run a computation, releasing its effects into the environment.

Instances

HasAnonBind l => MapBoundX GCast l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GCast l -> GCast l Source #
ShowLanguage l => Show (GCast l) Source #
Methods showsPrec :: Int -> GCast l -> ShowS # show :: GCast l -> String # showList :: [GCast l] -> ShowS #

type Witness = GWitness Source Source #

data GWitness l Source #

Witnesses.

Constructors

WAnnot !(GXAnnot l) !(GWitness l)	Witness annotation
WVar !(GXBoundVar l)	Witness variable.
WCon !(GWiCon l)	Witness constructor.
WApp !(GWitness l) !(GWitness l)	Witness application.
WType !(GType l)	Type can appear as an argument of a witness application.

Instances

HasAnonBind l => MapBoundX GWitness l Source #
Methods mapBoundAtDepthX :: l -> (Int -> GXBoundVar l -> GXBoundVar l) -> Int -> GWitness l -> GWitness l Source #
ShowLanguage l => Show (GWitness l) Source #
Methods showsPrec :: Int -> GWitness l -> ShowS # show :: GWitness l -> String # showList :: [GWitness l] -> ShowS #

type WiCon = GWiCon Source Source #

data GWiCon l Source #

Witness constructors.

Constructors

WiConBound !(GXBoundVar l) !(GType l)

Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed.

Instances

ShowLanguage l => Show (GWiCon l) Source #
Methods showsPrec :: Int -> GWiCon l -> ShowS # show :: GWiCon l -> String # showList :: [GWiCon l] -> ShowS #

data DaCon n t :: * -> * -> * #

Data constructors.

Constructors

DaConUnit	Baked in unit data constructor.
DaConPrim	Primitive data constructor used for literals and baked-in constructors. The type of the constructor needs to be attached to handle the case where there are too many constructors in the data type to list, like for Int literals. In this case we determine what data type it belongs to from the attached type of the data constructor.
Fields daConName :: ~n Name of the data constructor. daConType :: ~t Type of the data constructor.
DaConBound	Data constructor that has a data type declaration.
Fields daConName :: ~n Name of the data constructor.

Instances

(Eq n, Eq t) => Eq (DaCon n t)
Methods (==) :: DaCon n t -> DaCon n t -> Bool # (/=) :: DaCon n t -> DaCon n t -> Bool #
(Show n, Show t) => Show (DaCon n t)
Methods showsPrec :: Int -> DaCon n t -> ShowS # show :: DaCon n t -> String # showList :: [DaCon n t] -> ShowS #
(NFData n, NFData t) => NFData (DaCon n t)
Methods rnf :: DaCon n t -> () #

data DaConBind Source #

Binding occurrence of a data constructor.

Constructors

DaConBindName Text

Instances

Eq DaConBind Source #
Methods (==) :: DaConBind -> DaConBind -> Bool # (/=) :: DaConBind -> DaConBind -> Bool #
Ord DaConBind Source #
Methods compare :: DaConBind -> DaConBind -> Ordering # (<) :: DaConBind -> DaConBind -> Bool # (<=) :: DaConBind -> DaConBind -> Bool # (>) :: DaConBind -> DaConBind -> Bool # (>=) :: DaConBind -> DaConBind -> Bool # max :: DaConBind -> DaConBind -> DaConBind # min :: DaConBind -> DaConBind -> DaConBind #
Show DaConBind Source #
Methods showsPrec :: Int -> DaConBind -> ShowS # show :: DaConBind -> String # showList :: [DaConBind] -> ShowS #

data DaConBound Source #

Bound occurrences of a data constructor.

Constructors

DaConBoundName Text
DaConBoundLit PrimLit

Instances

Eq DaConBound Source #
Methods (==) :: DaConBound -> DaConBound -> Bool # (/=) :: DaConBound -> DaConBound -> Bool #
Ord DaConBound Source #
Methods compare :: DaConBound -> DaConBound -> Ordering # (<) :: DaConBound -> DaConBound -> Bool # (<=) :: DaConBound -> DaConBound -> Bool # (>) :: DaConBound -> DaConBound -> Bool # (>=) :: DaConBound -> DaConBound -> Bool # max :: DaConBound -> DaConBound -> DaConBound # min :: DaConBound -> DaConBound -> DaConBound #
Show DaConBound Source #
Methods showsPrec :: Int -> DaConBound -> ShowS # show :: DaConBound -> String # showList :: [DaConBound] -> ShowS #

Primitives

data PrimVal Source #

Primitive values.

Constructors

PrimValLit !PrimLit	Primitive literals.
PrimValArith !PrimArith	Primitive arithmetic operators.
PrimValCast !PrimCast	Primitive numeric casting operators.
PrimValError !OpError	Primitive error handling.
PrimValVector !OpVector	Primitive vector operators.
PrimValFun !OpFun	Primitive function operators.

Instances

Eq PrimVal Source #
Methods (==) :: PrimVal -> PrimVal -> Bool # (/=) :: PrimVal -> PrimVal -> Bool #
Ord PrimVal Source #
Methods compare :: PrimVal -> PrimVal -> Ordering # (<) :: PrimVal -> PrimVal -> Bool # (<=) :: PrimVal -> PrimVal -> Bool # (>) :: PrimVal -> PrimVal -> Bool # (>=) :: PrimVal -> PrimVal -> Bool # max :: PrimVal -> PrimVal -> PrimVal # min :: PrimVal -> PrimVal -> PrimVal #
Show PrimVal Source #
Methods showsPrec :: Int -> PrimVal -> ShowS # show :: PrimVal -> String # showList :: [PrimVal] -> ShowS #

data PrimArith :: * #

Primitive arithmetic, logic, and comparison opretors. We expect the backend/machine to be able to implement these directly.

For the Shift Right operator, the type that it is used at determines whether it is an arithmetic (with sign-extension) or logical (no sign-extension) shift.

Constructors

PrimArithNeg	Negation
PrimArithAdd	Addition
PrimArithSub	Subtraction
PrimArithMul	Multiplication
PrimArithDiv	Division
PrimArithMod	Modulus
PrimArithRem	Remainder
PrimArithEq	Equality
PrimArithNeq	Negated Equality
PrimArithGt	Greater Than
PrimArithGe	Greater Than or Equal
PrimArithLt	Less Than
PrimArithLe	Less Than or Equal
PrimArithAnd	Boolean And
PrimArithOr	Boolean Or
PrimArithShl	Shift Left
PrimArithShr	Shift Right
PrimArithBAnd	Bit-wise And
PrimArithBOr	Bit-wise Or
PrimArithBXOr	Bit-wise eXclusive Or

Instances

Eq PrimArith
Methods (==) :: PrimArith -> PrimArith -> Bool # (/=) :: PrimArith -> PrimArith -> Bool #
Ord PrimArith
Methods compare :: PrimArith -> PrimArith -> Ordering # (<) :: PrimArith -> PrimArith -> Bool # (<=) :: PrimArith -> PrimArith -> Bool # (>) :: PrimArith -> PrimArith -> Bool # (>=) :: PrimArith -> PrimArith -> Bool # max :: PrimArith -> PrimArith -> PrimArith # min :: PrimArith -> PrimArith -> PrimArith #
Show PrimArith
Methods showsPrec :: Int -> PrimArith -> ShowS # show :: PrimArith -> String # showList :: [PrimArith] -> ShowS #
Pretty PrimArith
Associated Types data PrettyMode PrimArith :: * # Methods pprDefaultMode :: PrettyMode PrimArith # ppr :: PrimArith -> Doc # pprPrec :: Int -> PrimArith -> Doc # pprModePrec :: PrettyMode PrimArith -> Int -> PrimArith -> Doc #
NFData PrimArith
Methods rnf :: PrimArith -> () #

data OpVector :: * #

Vector operators.

Constructors

OpVectorAlloc	Allocate a new vector of a given length number of elements.
OpVectorLength	Get the length of a vector, in elements.
OpVectorRead	Read a value from a vector.
OpVectorWrite	Write a value to a vector.

Instances

Eq OpVector
Methods (==) :: OpVector -> OpVector -> Bool # (/=) :: OpVector -> OpVector -> Bool #
Ord OpVector
Methods compare :: OpVector -> OpVector -> Ordering # (<) :: OpVector -> OpVector -> Bool # (<=) :: OpVector -> OpVector -> Bool # (>) :: OpVector -> OpVector -> Bool # (>=) :: OpVector -> OpVector -> Bool # max :: OpVector -> OpVector -> OpVector # min :: OpVector -> OpVector -> OpVector #
Show OpVector
Methods showsPrec :: Int -> OpVector -> ShowS # show :: OpVector -> String # showList :: [OpVector] -> ShowS #

data OpFun :: * #

Operators for building function values and closures. The implicit versions work on functions of type (a -> b), while the explicit versions use expliciy closure types like C# (a -> b).

Constructors

OpFunCurry Int	Partially apply a supecombinator to some arguments, producing an implicitly typed closure.
OpFunApply Int	Apply an implicitly typed closure to some more arguments.
OpFunCReify	Reify a function into an explicit functional value.
OpFunCCurry Int	Apply an explicit functional value to some arguments, producing an explicitly typed closure.
OpFunCExtend Int	Extend an explicitly typed closure with more arguments, producing a new closure.
OpFunCApply Int	Apply an explicitly typed closure to some arguments, possibly evaluating the contained function.

Instances

Eq OpFun
Methods (==) :: OpFun -> OpFun -> Bool # (/=) :: OpFun -> OpFun -> Bool #
Ord OpFun
Methods compare :: OpFun -> OpFun -> Ordering # (<) :: OpFun -> OpFun -> Bool # (<=) :: OpFun -> OpFun -> Bool # (>) :: OpFun -> OpFun -> Bool # (>=) :: OpFun -> OpFun -> Bool # max :: OpFun -> OpFun -> OpFun # min :: OpFun -> OpFun -> OpFun #
Show OpFun
Methods showsPrec :: Int -> OpFun -> ShowS # show :: OpFun -> String # showList :: [OpFun] -> ShowS #

data OpError :: * #

Operators for runtime error reporting.

Constructors

OpErrorDefault

Raise an error due to inexhaustive case expressions.

Instances

Eq OpError
Methods (==) :: OpError -> OpError -> Bool # (/=) :: OpError -> OpError -> Bool #
Ord OpError
Methods compare :: OpError -> OpError -> Ordering # (<) :: OpError -> OpError -> Bool # (<=) :: OpError -> OpError -> Bool # (>) :: OpError -> OpError -> Bool # (>=) :: OpError -> OpError -> Bool # max :: OpError -> OpError -> OpError # min :: OpError -> OpError -> OpError #
Show OpError
Methods showsPrec :: Int -> OpError -> ShowS # show :: OpError -> String # showList :: [OpError] -> ShowS #

data PrimLit Source #

Constructors

PrimLitBool !Bool	A boolean literal.
PrimLitNat !Integer	A natural literal, with enough precision to count every heap object.
PrimLitInt !Integer	An integer literal, with enough precision to count every heap object.
PrimLitSize !Integer	An unsigned size literal, with enough precision to count every addressable byte of memory.
PrimLitWord !Integer !Int	A word literal, with the given number of bits precison.
PrimLitFloat !Double !Int	A floating point literal, with the given number of bits precision.
PrimLitChar !Char	A character literal.
PrimLitTextLit !Text	Text literals (UTF-8 encoded)

Instances

Eq PrimLit Source #
Methods (==) :: PrimLit -> PrimLit -> Bool # (/=) :: PrimLit -> PrimLit -> Bool #
Ord PrimLit Source #
Methods compare :: PrimLit -> PrimLit -> Ordering # (<) :: PrimLit -> PrimLit -> Bool # (<=) :: PrimLit -> PrimLit -> Bool # (>) :: PrimLit -> PrimLit -> Bool # (>=) :: PrimLit -> PrimLit -> Bool # max :: PrimLit -> PrimLit -> PrimLit # min :: PrimLit -> PrimLit -> PrimLit #
Show PrimLit Source #
Methods showsPrec :: Int -> PrimLit -> ShowS # show :: PrimLit -> String # showList :: [PrimLit] -> ShowS #

pattern PTrue :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t Source #

pattern PFalse :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t Source #

Dictionaries

type ShowLanguage l = (Show l, ShowGType l, Show (GXAnnot l), Show (GXBindVar l), Show (GXBoundVar l), Show (GXBindCon l), Show (GXBoundCon l), Show (GXPrim l)) Source #