- type Bind a = (Name, a)
- newtype Boxed = Boxed (Clos Term)
- type Clos a = (a, Scope)
- class Closure a where
- data Entry
- class Enum a
- class Env e where
- data EnvEntry
- type EnvEntries = [(EnvEntry, PrtInfo)]
- class GetLoc a where
- type Id = Int
- type Label = String
- data Loc
- type Name = String
- data Ne
- data Phrase
- data PiSigma
- type Prog = [Entry]
- data PrtInfo = PrtInfo {}
- newtype Scope = Scope [(Name, (Id, Maybe (Clos Type)))]
- data Term
- = Var Loc Name
- | Let Loc Prog Term
- | Type Loc
- | Q Loc PiSigma (Type, Bind Type)
- | Lam Loc (Bind Term)
- | App Term Term
- | Pair Loc Term Term
- | Split Loc Term (Bind (Bind Term))
- | Enum Loc [Name]
- | Label Loc Label
- | Case Loc Term [(Label, Term)]
- | Lift Loc Term
- | Box Loc Term
- | Force Loc Term
- | Rec Loc Term
- | Fold Loc Term
- | Unfold Loc Term (Bind Term)
- type Type = Term
- data Val
- (-*-) :: Type -> Type -> Type
- (->-) :: Type -> Type -> Type
- emptyScope :: Scope
- extendScope :: Scope -> Name -> (Id, Maybe (Clos Type)) -> Scope
- label :: Label -> Clos Term
- lam :: [(Loc, Name)] -> Term -> Term
- locMessage :: Loc -> String
- decls :: Prog -> [Name]
- lookupCon :: Scope -> Name -> Maybe (Clos Type)
- lookupScope :: Scope -> Name -> Maybe Id
- pis :: [(Loc, Name)] -> Type -> Type -> Type
- sigmas :: [(Loc, Name)] -> Type -> Type -> Type
- split :: Loc -> Term -> (Name, Name) -> Term -> Term
- ty :: Clos Type
- lty :: Clos Type
- tforce :: Clos Type -> Clos Type
- tlift :: Clos Type -> Clos Type
Documentation
class Enum a
Class Enum
defines operations on sequentially ordered types.
The enumFrom
... methods are used in Haskell's translation of
arithmetic sequences.
Instances of Enum
may be derived for any enumeration type (types
whose constructors have no fields). The nullary constructors are
assumed to be numbered left-to-right by fromEnum
from 0
through n-1
.
See Chapter 10 of the Haskell Report for more details.
For any type that is an instance of class Bounded
as well as Enum
,
the following should hold:
- The calls
andsucc
maxBound
should result in a runtime error.pred
minBound
-
fromEnum
andtoEnum
should give a runtime error if the result value is not representable in the result type. For example,
is an error.toEnum
7 ::Bool
-
enumFrom
andenumFromThen
should be defined with an implicit bound, thus:
enumFrom x = enumFromTo x maxBound
enumFromThen x y = enumFromThenTo x y bound
where
bound | fromEnum y >= fromEnum x = maxBound
| otherwise = minBound
type EnvEntries = [(EnvEntry, PrtInfo)]Source
Neutral terms.
Var Loc Name | |
Let Loc Prog Term | |
Type Loc | |
Q Loc PiSigma (Type, Bind Type) | |
Lam Loc (Bind Term) | |
App Term Term | |
Pair Loc Term Term | |
Split Loc Term (Bind (Bind Term)) | |
Enum Loc [Name] | |
Label Loc Label | |
Case Loc Term [(Label, Term)] | |
Lift Loc Term | |
Box Loc Term | |
Force Loc Term | |
Rec Loc Term | |
Fold Loc Term | |
Unfold Loc Term (Bind Term) |
locMessage :: Loc -> StringSource