Language.PiSigma.Syntax

Synopsis

Documentation

The use of Bind indicates the scope of the bound identifier.

Constructors

Instances

Eq Boxed
Show Boxed
Closure Boxed
Equal Boxed

type Clos a = (a, Scope)Source

class Closure a whereSource

Methods

getScope :: a -> Scope Source

putScope :: a -> Scope -> aSource

Instances

Closure Boxed
Closure (Clos a)
Closure a => Closure (Bind a)

data Entry Source

Constructors

Decl Loc Name Type
Defn Loc Name Term

Instances

Eq Entry
Show Entry
GetLoc Entry

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 succ maxBound and pred minBound should result in a runtime error.
fromEnum and toEnum should give a runtime error if the result value is not representable in the result type. For example, toEnum 7 :: Bool is an error.
enumFrom and enumFromThen 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

Instances

Enum Bool
Enum Char
Enum Double
Enum Float
Enum Int
Enum Integer
Enum Ordering
Enum ()
Enum GeneralCategory
Enum Message

class Env e whereSource

Methods

emptyE :: eSource

extE :: e -> PrtInfo -> (Id, e)Source

setE :: e -> Id -> EnvEntry -> eSource

getE :: e -> Id -> EnvEntry Source

prtE :: e -> Id -> PrtInfo Source

Instances

Env EnvEntries

data EnvEntry Source

Constructors

Id Id
Closure (Clos Term)

Instances

Show EnvEntry
Env EnvEntries

type EnvEntries = [(EnvEntry, PrtInfo)]Source

class GetLoc a whereSource

Methods

getLoc :: a -> Loc Source

Instances

GetLoc Term
GetLoc Entry
GetLoc a => GetLoc (Clos a)

type Id = Int Source

type Label = String Source

data Loc Source

Constructors

Unknown
Loc
Fields filename :: !String line :: !Int column :: !Int

Instances

Eq Loc	Locations are always equal. This allows us to derive equality for the abstract syntax that ignores the locations.
Show Loc

type Name = String Source

data Ne Source

Neutral terms.

Constructors

NVar Id
Ne :.. (Clos Term)
NSplit Ne (Bind (Bind (Clos Term)))
NCase Ne (Clos [(Label, Term)])
NForce Ne
NUnfold Ne (Bind (Clos Term))

Instances

Eq Ne
Show Ne
Print Ne
Equal Ne
Nf Ne Term

data Phrase Source

Constructors

Prog Prog
Term Term

Instances

Eq Phrase
Show Phrase

data PiSigma Source

For treating quantifiers in a uniform way.

Constructors

Pi
Sigma

Instances

Eq PiSigma
Show PiSigma

type Prog = [Entry]Source

data PrtInfo Source

Constructors

PrtInfo
Fields name :: Name expand :: Bool

Instances

Env EnvEntries

newtype Scope Source

Constructors

Scope [(Name, (Id, Maybe (Clos Type)))]

Instances

Eq Scope
Show Scope
Closure (Clos a)
GetLoc a => GetLoc (Clos a)
Print (Clos Term)
Equal (Clos Term)
Nf (Clos Term) Term

data Term Source

Constructors

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)

Instances

Eq Term
Show Term
GetLoc Term
Print Term
Nf Ne Term
Nf Val Term
Nf Id Term
Print (Clos Term)
Equal (Clos Term)
Nf (Clos Term) Term

type Type = Term Source

data Val Source

Constructors

Ne Ne
VType
VQ PiSigma (Clos (Type, Bind Type))
VLift (Clos Type)
VLam (Bind (Clos Term))
VPair (Clos (Term, Term))
VEnum [Label]
VLabel Label
VBox Boxed
VRec (Clos Type)
VFold (Clos Term)