Safe Haskell | None |
---|---|
Language | Haskell98 |
Definition of Source Tetra Abstract Syntax, and utilities for working with it.
- type Name = Text
- data Bind
- data Bound
- takeBoundOfBind :: Bind -> Maybe Bound
- type Type = GType Source
- data GType l :: * -> *
- type TyCon = GTyCon Source
- data GTyCon l :: * -> *
- = TyConVoid
- | TyConUnit
- | TyConFun
- | TyConUnion ~(GType l)
- | TyConBot ~(GType l)
- | TyConForall ~(GType l)
- | TyConExists ~(GType l)
- | TyConPrim ~(GTPrim l)
- | TyConBound ~(GTBoundCon l)
- data TyConBind = TyConBindName Text
- data TyConBound = TyConBoundName Text
- data Source = Source
- type family GTAnnot l :: *
- type family GTBindVar l :: *
- type family GTBoundVar l :: *
- type family GTBindCon l :: *
- type family GTBoundCon l :: *
- type family GTPrim l :: *
- data SoCon :: *
- data KiCon :: *
- data TwCon :: *
- data TcCon :: *
- data PrimType
- data PrimTyCon :: *
- data PrimTyConTetra
- pattern TApp2 :: forall t. GType t -> GType t -> GType t -> GType t
- pattern TApp3 :: forall t. GType t -> GType t -> GType t -> GType t -> GType t
- pattern TApp4 :: forall t. GType t -> GType t -> GType t -> GType t -> GType t -> GType t
- pattern TApp5 :: forall t. GType t -> GType t -> GType t -> GType t -> GType t -> GType t -> GType t
- pattern TVoid :: forall t. GType t
- pattern TUnit :: forall t. GType t
- pattern TFun :: forall t. GType t -> GType t -> GType t
- pattern TBot :: forall t. GType t -> GType t
- pattern TUnion :: forall t. GType t -> GType t -> GType t -> GType t
- pattern TPrim :: forall t. GTPrim t -> GType t
- pattern KData :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern KRegion :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern KEffect :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TImpl :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t
- pattern TSusp :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t -> GType t
- pattern TRead :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t
- pattern TWrite :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t
- pattern TAlloc :: forall t. (~#) * * (GTPrim t) PrimType => GType t -> GType t
- pattern TBool :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TNat :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TInt :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TSize :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- pattern TWord :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t
- pattern TFloat :: forall t. (~#) * * (GTPrim t) PrimType => Int -> GType t
- pattern TTextLit :: forall t. (~#) * * (GTPrim t) PrimType => GType t
- isAtomT :: GType l -> Bool
- takeTCon :: GType l -> Maybe (GTyCon l)
- takeTVar :: GType l -> Maybe (GTBoundVar l)
- takeTAbs :: GType l -> Maybe (GTBindVar l, GType l, GType l)
- takeTApp :: GType l -> Maybe (GType l, GType l)
- makeTApps :: GType l -> [GType l] -> GType l
- takeTApps :: GType l -> [GType l]
- makeTFun :: GType l -> GType l -> GType l
- makeTFuns :: [GType l] -> GType l -> GType l
- makeTFuns' :: [GType l] -> Maybe (GType l)
- (~>) :: GType l -> GType l -> GType l
- takeTFun :: GType l -> Maybe (GType l, GType l)
- takeTFuns :: GType l -> ([GType l], GType l)
- takeTFuns' :: GType l -> [GType l]
- makeTForall :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l
- makeTForalls :: Anon l => l -> [GType l] -> ([GType l] -> GType l) -> GType l
- takeTForall :: GType l -> Maybe (GType l, GTBindVar l, GType l)
- makeTExists :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l
- takeTExists :: GType l -> Maybe (GType l, GTBindVar l, GType l)
- takeTUnion :: GType l -> Maybe (GType l, GType l, GType l)
- makeTUnions :: GType l -> [GType l] -> GType l
- takeTUnions :: Eq (GType l) => GType l -> Maybe (GType l, [GType l])
- splitTUnionsOfKind :: Eq (GType l) => GType l -> GType l -> Maybe [GType l]
- makeTBot :: GType l -> GType l
- type Annot = GXAnnot Source
- type family GXAnnot l
- type BindVar = GXBindVar Source
- type family GXBindVar l
- type BindVarMT = GXBindVarMT Source
- data GXBindVarMT l = XBindVarMT (GXBindVar l) (Maybe (GType l))
- type BoundVar = GXBoundVar Source
- type family GXBoundVar l
- type BindCon = GXBoundCon Source
- type family GXBindCon l
- type BoundCon = GXBoundCon Source
- type family GXBoundCon l
- type Prim = GXPrim Source
- type family GXPrim l
- type Exp = GExp Source
- data GExp l
- = XAnnot !(GXAnnot l) !(GExp l)
- | XVar !(GXBoundVar l)
- | XPrim !(GXPrim l)
- | XCon !(DaCon (GXBoundCon l) (GType l))
- | XLAM !(GXBindVarMT l) !(GExp l)
- | XLam !(GXBindVarMT l) !(GExp l)
- | XApp !(GExp l) !(GExp l)
- | XLet !(GLets l) !(GExp l)
- | XCase !(GExp l) ![GAltCase l]
- | XCast !(GCast l) !(GExp l)
- | XType !(GType l)
- | XWitness !(GWitness l)
- | XDefix !(GXAnnot l) [GExp l]
- | XInfixOp !(GXAnnot l) String
- | XInfixVar !(GXAnnot l) String
- | XMatch !(GXAnnot l) ![GAltMatch l] !(GExp l)
- | XWhere !(GXAnnot l) !(GExp l) ![GClause l]
- | XLamPat !(GXAnnot l) !(GPat l) !(Maybe (GType l)) !(GExp l)
- | XLamCase !(GXAnnot l) ![GAltCase l]
- type Lets = GLets Source
- data GLets l
- type Clause = GClause Source
- data GClause l
- = SSig !(GXAnnot l) !(GXBindVar l) !(GType l)
- | SLet !(GXAnnot l) !(GXBindVarMT l) ![GParam l] ![GGuardedExp l]
- type Param = GParam Source
- data GParam l
- type Pat = GPat Source
- data GPat l
- type Guard = GGuard Source
- data GGuard l
- type GuardedExp = GGuardedExp Source
- data GGuardedExp l
- = GGuard !(GGuard l) !(GGuardedExp l)
- | GExp !(GExp l)
- type AltCase = GAltCase Source
- data GAltCase l = AAltCase !(GPat l) ![GGuardedExp l]
- type AltMatch = GAltMatch Source
- data GAltMatch l = AAltMatch !(GGuardedExp l)
- type Cast = GCast Source
- data GCast l
- = CastWeakenEffect !(GType l)
- | CastPurify !(GWitness l)
- | CastBox
- | CastRun
- type Witness = GWitness Source
- data GWitness l
- type WiCon = GWiCon Source
- data GWiCon l = WiConBound !(GXBoundVar l) !(GType l)
- data DaCon n t :: * -> * -> *
- data DaConBind = DaConBindName Text
- data DaConBound
- = DaConBoundName Text
- | DaConBoundLit PrimLit
- data PrimVal
- data PrimArith :: *
- data OpVector :: *
- data OpFun :: *
- data OpError :: * = OpErrorDefault
- data PrimLit
- = PrimLitBool !Bool
- | PrimLitNat !Integer
- | PrimLitInt !Integer
- | PrimLitSize !Integer
- | PrimLitWord !Integer !Int
- | PrimLitFloat !Double !Int
- | PrimLitChar !Char
- | PrimLitTextLit !Text
- pattern PTrue :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t
- pattern PFalse :: forall t. ((~#) * * (GTPrim t) PrimType, (~#) * * (GXBoundCon t) DaConBound) => GPat t
- isXVar :: GExp l -> Bool
- isXCon :: GExp l -> Bool
- isAtomX :: GExp l -> Bool
- isAtomW :: GWitness l -> Bool
- isXLAM :: GExp l -> Bool
- isXLam :: GExp l -> Bool
- isLambdaX :: GExp l -> Bool
- isXApp :: GExp l -> Bool
- isXLet :: GExp l -> Bool
- isXType :: GExp l -> Bool
- isXWitness :: GExp l -> Bool
- isPDefault :: GPat l -> Bool
- takeAnnotOfExp :: GExp l -> Maybe (GXAnnot l)
- bindOfBindMT :: GXBindVarMT l -> GXBindVar l
- takeTypeOfBindMT :: GXBindVarMT l -> Maybe (GType l)
- makeXLAMs :: [GXBindVarMT l] -> GExp l -> GExp l
- makeXLams :: [GXBindVarMT l] -> GExp l -> GExp l
- makeXLamFlags :: [(Bool, GXBindVarMT l)] -> GExp l -> GExp l
- takeXLAMs :: GExp l -> Maybe ([GXBindVarMT l], GExp l)
- takeXLams :: GExp l -> Maybe ([GXBindVarMT l], GExp l)
- takeXLamFlags :: GExp l -> Maybe ([(Bool, GXBindVarMT l)], GExp l)
- makeXApps :: GExp l -> [GExp l] -> GExp l
- makeXAppsWithAnnots :: GExp l -> [(GExp l, Maybe (GXAnnot l))] -> GExp l
- takeXApps :: GExp l -> Maybe (GExp l, [GExp l])
- takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l])
- takeXAppsAsList :: GExp l -> [GExp l]
- takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, Maybe (GXAnnot l))])
- takeXConApps :: GExp l -> Maybe (DaCon (GXBoundCon l) (GType l), [GExp l])
- takeXPrimApps :: GExp l -> Maybe (GXPrim l, [GExp l])
- bindOfClause :: GClause l -> GXBindVar l
- pattern XRun :: forall t. GExp t -> GExp t
- pattern XBox :: forall t. GExp t -> GExp t
- dcUnit :: DaCon n t
- takeNameOfDaCon :: DaCon n t -> Maybe n
- takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n)
- bindsOfPat :: Pat n -> [Bind n]
- wApp :: a -> Witness a n -> Witness a n -> Witness a n
- wApps :: a -> Witness a n -> [Witness a n] -> Witness a n
- takeXWitness :: Exp a n -> Maybe (Witness a n)
- takeWAppsAsList :: Witness a n -> [Witness a n]
- takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])
- 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))
- type PrettyLanguage l = (Pretty l, Pretty (GTAnnot l), Pretty (GTBindVar l), Pretty (GTBoundVar l), Pretty (GTBindCon l), Pretty (GTBoundCon l), Pretty (GTPrim l), Pretty (GXAnnot l), Pretty (GXBindVar l), Pretty (GXBoundVar l), Pretty (GXBindCon l), Pretty (GXBoundCon l), Pretty (GXPrim l), Pretty (DaCon (GXBoundCon l) (GType l)))
- type NFDataLanguage l = (NFData l, NFDataLanguage l, NFData (GXAnnot l), NFData (GXBindVar l), NFData (GXBoundVar l), NFData (GXBindCon l), NFData (GXBoundCon l), NFData (GXPrim l))
Binding
Binding occurrence of a variable.
Bound occurrence of a variable.
Types
Syntax
Expressions
Generic type expression representation.
TyCons
Wrapper for primitive constructors that adds the ones common to SystemFω based languages.
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. |
Binding occurrence of a type constructor.
TyConBindName Text |
Type Generics
Type index for Source Tetra Language.
Show Source Source # | |
Pretty Source Source # | |
Anon Source Source # | |
HasAnonBind Source Source # | |
Expand AltMatch Source # | |
Expand AltCase Source # | |
Expand GuardedExp Source # | |
Expand Guard Source # | |
Expand Clause Source # | |
Expand Exp Source # | |
Expand (Top Source) Source # | |
Expand (Module Source) Source # | |
type GTAnnot Source Source # | |
type GTBindVar Source Source # | |
type GTBoundVar Source Source # | |
type GTBindCon Source Source # | |
type GTBoundCon Source Source # | |
type GTPrim Source Source # | |
type GXPrim Source Source # | |
type GXBoundCon Source Source # | |
type GXBindCon Source Source # | |
type GXBoundVar Source Source # | |
type GXBindVar Source Source # | |
type GXAnnot Source Source # | |
type family GTBoundVar l :: * #
Yield the type of bound occurrences of variables.
type GTBoundVar Source # | |
type family GTBoundCon l :: * #
Yield the type of bound occurrences of constructors.
type GTBoundCon Source # | |
Type Constructors
Sort constructor.
Kind constructor.
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. |
Witness type 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. |
Other constructors at the spec level.
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. |
Type Primitives
Primitive types.
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. |
Primitive type constructors.
PrimTyConVoid |
|
PrimTyConBool |
|
PrimTyConNat |
|
PrimTyConInt |
|
PrimTyConSize |
|
PrimTyConWord Int |
|
PrimTyConFloat Int |
|
PrimTyConVec Int |
|
PrimTyConAddr |
|
PrimTyConPtr |
|
PrimTyConTextLit |
|
PrimTyConTag |
|
data PrimTyConTetra Source #
Primitive type constructors specific to the Tetra language fragment.
PrimTyConTetraTuple !Int |
|
PrimTyConTetraVector |
|
PrimTyConTetraF |
|
PrimTyConTetraC |
|
PrimTyConTetraU |
|
Pattern Synonyms
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 TUnion :: forall t. GType t -> GType t -> GType t -> GType t #
Representation of a union of two types.
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 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.
Predicates
Compounds
Destructors
takeTVar :: GType l -> Maybe (GTBoundVar l) #
Take a type variable, looking through annotations.
takeTAbs :: GType l -> Maybe (GTBindVar l, GType l, GType l) #
Take a type abstraction, looking through annotations.
takeTApp :: GType l -> Maybe (GType l, GType l) #
Take a type application, looking through annotations.
Type Applications
takeTApps :: GType l -> [GType l] #
Flatten a sequence of type applications into the function part and arguments, if any.
Function Types
makeTFun :: GType l -> GType l -> GType l infixr 9 #
Construct a function type with the given parameter and result type.
makeTFuns' :: [GType l] -> Maybe (GType l) #
Like makeTFuns
but taking the parameter and return types as a list.
takeTFun :: GType l -> Maybe (GType l, GType l) #
Destruct a function type into its parameter and result types,
returning Nothing
if this isn't a function type.
takeTFuns :: GType l -> ([GType l], GType l) #
Destruct a function type into into all its parameters and result type, returning an empty parameter list if this isn't a function type.
takeTFuns' :: GType l -> [GType l] #
Like takeFuns
, but yield the parameter and return types in the same list.
Forall Types
makeTForall :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l #
Construct a forall quantified type using an anonymous binder.
makeTForalls :: Anon l => l -> [GType l] -> ([GType l] -> GType l) -> GType l #
Construct a forall quantified type using some anonymous binders.
takeTForall :: GType l -> Maybe (GType l, GTBindVar l, GType l) #
Destruct a forall quantified type, if this is one.
The kind we return comes from the abstraction rather than the Forall constructor.
Exists Types
makeTExists :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l #
Construct an exists quantified type using an anonymous binder.
takeTExists :: GType l -> Maybe (GType l, GTBindVar l, GType l) #
Destruct an exists quantified type, if this is one.
The kind we return comes from the abstraction rather than the Exists constructor.
Union types
takeTUnion :: GType l -> Maybe (GType l, GType l, GType l) #
Take the kind, left and right types from a union type.
makeTUnions :: GType l -> [GType l] -> GType l #
Make a union type from a kind and list of component types.
takeTUnions :: Eq (GType l) => GType l -> Maybe (GType l, [GType l]) #
Split a union type into its components. If this is not a union, or is an ill kinded union then Nothing.
splitTUnionsOfKind :: Eq (GType l) => GType l -> GType l -> Maybe [GType l] #
Split a union of the given kind into its components. When we split a sum we need to check that the kind attached to the sum type constructor is the one that we were expecting, otherwise we risk splitting ill-kinded sums without noticing it.
Terms
Syntax
type BindVarMT = GXBindVarMT Source Source #
data GXBindVarMT l Source #
A possibly typed binding.
XBindVarMT (GXBindVar l) (Maybe (GType l)) |
ShowLanguage l => Show (GXBindVarMT l) Source # | |
type BoundVar = GXBoundVar Source Source #
type family GXBoundVar l Source #
Yield the type of bound occurrences of variables.
type GXBoundVar Source Source # | |
type BindCon = GXBoundCon Source Source #
type BoundCon = GXBoundCon Source Source #
type family GXBoundCon l Source #
Yield the type of bound occurrences of constructors.
type GXBoundCon Source Source # | |
Yield the type of primitive operator names.
Expressions
Well-typed expressions have types of kind Data
.
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. |
Let-binding
Possibly recursive bindings. Whether these are taken as recursive depends on whether they appear in an XLet or XLetrec group.
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. |
Clauses
Binding clause
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. |
Parameters
Parameter for a binding.
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. |
ShowLanguage l => Show (GParam l) Source # | |
Patterns
Patterns.
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. |
ShowLanguage l => Show (GPat l) Source # | |
Guards
Expression guards.
Guarded Expressions
type GuardedExp = GGuardedExp Source Source #
data GGuardedExp l Source #
An expression with some guards.
GGuard !(GGuard l) !(GGuardedExp l) | |
GExp !(GExp l) |
Expand GuardedExp Source # | |
HasAnonBind l => MapBoundX GGuardedExp l Source # | |
Defix GGuardedExp l Source # | |
ShowLanguage l => Show (GGuardedExp l) Source # | |
Case Alternatives
Case alternative. If the pattern matches then bind the variables then enter the guarded expression.
AAltCase !(GPat l) ![GGuardedExp l] |
Match alternative. This is like a case alternative except that the match expression does not give us a head pattern.
AAltMatch !(GGuardedExp l) |
Casts
Type casts.
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. |
HasAnonBind l => MapBoundX GCast l Source # | |
ShowLanguage l => Show (GCast l) Source # | |
Witnesses
Witnesses.
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. |
HasAnonBind l => MapBoundX GWitness l Source # | |
ShowLanguage l => Show (GWitness l) Source # | |
Witness Constructors
Witness 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. |
ShowLanguage l => Show (GWiCon l) Source # | |
Data Constructors
data DaCon n t :: * -> * -> * #
Data 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. |
DaConBound | Data constructor that has a data type declaration. |
|
Binding occurrence of a data constructor.
DaConBindName Text |
data DaConBound Source #
Bound occurrences of a data constructor.
Term Primitives
Primitive values.
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. |
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.
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 |
Vector operators.
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. |
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).
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. |
Operators for runtime error reporting.
OpErrorDefault | Raise an error due to inexhaustive case expressions. |
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) |
Pattern Synonyms
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 #
Predicates
Atoms
Lambdas
isXLam :: GExp l -> Bool Source #
Check whether an expression is a value or witness abstraction (level-0).
isLambdaX :: GExp l -> Bool Source #
Check whether an expression is a spec, value, or witness abstraction.
Applications
Let bindings
Types and Witnesses
Patterns
Compounds
Binds
bindOfBindMT :: GXBindVarMT l -> GXBindVar l Source #
Take the GBind
of a GBindMT
takeTypeOfBindMT :: GXBindVarMT l -> Maybe (GType l) Source #
Take the type of a GBindMT
.
Lambdas
makeXLamFlags :: [(Bool, GXBindVarMT l)] -> GExp l -> GExp l Source #
Make some nested lambda abstractions, using a flag to indicate whether the lambda is a level-1 (True), or level-0 (False) binder.
takeXLAMs :: GExp l -> Maybe ([GXBindVarMT l], GExp l) Source #
Split type lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLams :: GExp l -> Maybe ([GXBindVarMT l], GExp l) Source #
Split nested value or witness lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLamFlags :: GExp l -> Maybe ([(Bool, GXBindVarMT l)], GExp l) Source #
Split nested lambdas from the front of an expression, with a flag indicating whether the lambda was a level-1 (True), or level-0 (False) binder.
Applications
makeXAppsWithAnnots :: GExp l -> [(GExp l, Maybe (GXAnnot l))] -> GExp l Source #
Build sequence of applications.
Similar to xApps
but also takes list of annotations for
the XApp
constructors.
takeXApps :: GExp l -> Maybe (GExp l, [GExp l]) Source #
Flatten an application into the function part and its arguments.
Returns Nothing
if there is no outer application.
takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l]) Source #
Flatten an application into the function part and its arguments.
This is like takeXApps
above, except we know there is at least one argument.
takeXAppsAsList :: GExp l -> [GExp l] Source #
Flatten an application into the function parts and arguments, if any.
takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, Maybe (GXAnnot l))]) Source #
Destruct sequence of applications.
Similar to takeXAppsAsList
but also keeps annotations for later.
takeXConApps :: GExp l -> Maybe (DaCon (GXBoundCon l) (GType l), [GExp l]) Source #
Flatten an application of a data constructor into the constructor and its arguments.
Returns Nothing
if the expression isn't a constructor application.
takeXPrimApps :: GExp l -> Maybe (GXPrim l, [GExp l]) Source #
Flatten an application of a primop into the variable and its arguments.
Returns Nothing
if the expression isn't a primop application.
Clauses
bindOfClause :: GClause l -> GXBindVar l Source #
Take the binding variable of a clause.
Casts
Data Constructors
takeNameOfDaCon :: DaCon n t -> Maybe n #
Take the name of data constructor, if there is one.
takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n) #
Take the type annotation of a data constructor, if we know it locally.
Patterns
bindsOfPat :: Pat n -> [Bind n] #
Take the binds of a Pat
.
Witnesses
wApps :: a -> Witness a n -> [Witness a n] -> Witness a n #
Construct a sequence of witness applications
takeWAppsAsList :: Witness a n -> [Witness a n] #
Flatten an application into the function parts and arguments, if any.
takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n]) #
Flatten an application of a witness into the witness constructor name and its arguments.
Returns nothing if there is no witness constructor in head position.
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 #
type PrettyLanguage l = (Pretty l, Pretty (GTAnnot l), Pretty (GTBindVar l), Pretty (GTBoundVar l), Pretty (GTBindCon l), Pretty (GTBoundCon l), Pretty (GTPrim l), Pretty (GXAnnot l), Pretty (GXBindVar l), Pretty (GXBoundVar l), Pretty (GXBindCon l), Pretty (GXBoundCon l), Pretty (GXPrim l), Pretty (DaCon (GXBoundCon l) (GType l))) Source #
type NFDataLanguage l = (NFData l, NFDataLanguage l, NFData (GXAnnot l), NFData (GXBindVar l), NFData (GXBoundVar l), NFData (GXBindCon l), NFData (GXBoundCon l), NFData (GXPrim l)) Source #