Safe Haskell	None
Language	Haskell98

Value

Contents

Sizes ------------------------------------------------------------
destructors -------------------------------------------------------
ugly printing -----------------------------------------------------

Synopsis

data Val
- = VInfty
- | VZero
- | VSucc Val
- | VMax [Val]
- | VPlus [Val]
- | VMeta MVar Env Int
- | VSort (Sort Val)
- | VMeasured (Measure Val) Val
- | VGuard (Bound Val) Val
- | VBelow LtLe Val
- | VQuant {
  - vqPiSig :: PiSigma
  - vqName :: Name
  - vqDom :: Domain
  - vqFun :: FVal
  }
- | VSing Val TVal
- | VLam Name Env Expr
- | VAbs Name Int Val Valuation
- | VConst Val
- | VUp Val TVal
- | VRecord RecInfo EnvMap
- | VPair Val Val
- | VGen Int
- | VDef DefId
- | VCase Val TVal Env [Clause]
- | VApp Val [Clos]
- | VProj PrePost Name
- | VClos Env Expr
- | VIrr
vLam :: Name -> Env -> Expr -> FVal
isFun :: Val -> Bool
absName :: FVal -> Name
type FVal = Val
type TVal = Val
type Clos = Val
type Domain = Dom TVal
newtype Valuation = Valuation {
- valuation :: [(Int, Val)]
}
emptyVal :: Valuation
sgVal :: Int -> Val -> Valuation
valuateGen :: Int -> Valuation -> Val
type TeleVal = [TBinding Val]
data Environ a = Environ {
- envMap :: [(Name, a)]
- envBound :: Maybe (Measure Val)
}
type EnvMap = [(Name, Val)]
type Env = Environ Val
vSize :: Val
vFinSize :: Val
vSort :: Sort Val -> Val
isVSize :: Val -> Bool
vTSize :: Val
vTopSort :: Val
mkClos :: Env -> Expr -> Val
filterEnv :: Set Name -> EnvMap -> EnvMap
vDef :: DefId -> Val
vCon :: ConK -> QName -> Val
vFun :: Name -> Val
vDat :: QName -> Val
vAbs :: Name -> Int -> Val -> FVal
arrow :: TVal -> TVal -> TVal
prod :: TVal -> TVal -> TVal
quant :: PiSigma -> TVal -> Val -> Val
succSize :: Val -> Val
vSucc :: Val -> Val
plusSize :: Val -> Val -> Val
plusSizes :: [Val] -> Val
maxSize :: [Val] -> Val
vSortToSort :: Sort Val -> Sort Expr
predSize :: Val -> Maybe Val
isFunType :: TVal -> Bool
isDataType :: TVal -> Bool
showSkipLambda :: Val -> String
showVals :: [Val] -> String
emptyEnv :: Environ a
appendEnv :: Environ a -> Environ a -> Environ a
update :: Environ a -> Name -> a -> Environ a
lookupPure :: Show a => Environ a -> Name -> a
lookupEnv :: MonadError TraceError m => Environ a -> Name -> m a
showValuation :: Valuation -> String
showEnv :: Environ Val -> String
showEnv' :: EnvMap -> String

Documentation

data Val Source #

Constructors

VInfty
VZero
VSucc Val
VMax [Val]
VPlus [Val]
VMeta MVar Env Int
VSort (Sort Val)
VMeasured (Measure Val) Val
VGuard (Bound Val) Val
VBelow LtLe Val
VQuant
Fields vqPiSig :: PiSigma vqName :: Name vqDom :: Domain vqFun :: FVal
VSing Val TVal
VLam Name Env Expr
VAbs Name Int Val Valuation
VConst Val
VUp Val TVal
VRecord RecInfo EnvMap
VPair Val Val
VGen Int
VDef DefId
VCase Val TVal Env [Clause]
VApp Val [Clos]
VProj PrePost Name
VClos Env Expr
VIrr

Instances

Instances details

HasPred Val Source #
Instance details Defined in Value Methods predecessor :: Val -> Maybe Val Source #
Nocc Val Source #
Instance details Defined in Eval Methods nocc :: [Int] -> Val -> TypeCheck Bool Source #
Reval Env Source #
Instance details Defined in Eval Methods reval' :: Valuation -> Env -> TypeCheck Env Source # reval :: Env -> TypeCheck Env Source #
Reval Val Source #
Instance details Defined in Eval Methods reval' :: Valuation -> Val -> TypeCheck Val Source # reval :: Val -> TypeCheck Val Source #
PrettyTCM Val Source #
Instance details Defined in PrettyTCM Methods prettyTCM :: Val -> TypeCheck Doc Source #
ToExpr Val Source #
Instance details Defined in PrettyTCM Methods toExpression :: Val -> TypeCheck Expr Source #
Substitute Env Source #	Substitute in environment.
Instance details Defined in TypeChecker Methods substitute :: Substitution -> Env -> TypeCheck Env Source #
Substitute Val Source #
Instance details Defined in TypeChecker Methods substitute :: Substitution -> Val -> TypeCheck Val Source #
Show Val Source #
Instance details Defined in Value Methods showsPrec :: Int -> Val -> ShowS # show :: Val -> String # showList :: [Val] -> ShowS #
Eq Val Source #
Instance details Defined in Value Methods (==) :: Val -> Val -> Bool # (/=) :: Val -> Val -> Bool #
Ord Val Source #
Instance details Defined in Value Methods compare :: Val -> Val -> Ordering # (<) :: Val -> Val -> Bool # (<=) :: Val -> Val -> Bool # (>) :: Val -> Val -> Bool # (>=) :: Val -> Val -> Bool # max :: Val -> Val -> Val # min :: Val -> Val -> Val #
PrettyTCM (Sort Val) Source #
Instance details Defined in PrettyTCM Methods prettyTCM :: Sort Val -> TypeCheck Doc Source #
PrettyTCM [Val] Source #
Instance details Defined in PrettyTCM Methods prettyTCM :: [Val] -> TypeCheck Doc Source #
Show (Sort Val) Source #
Instance details Defined in Value Methods showsPrec :: Int -> Sort Val -> ShowS # show :: Sort Val -> String # showList :: [Sort Val] -> ShowS #

vLam :: Name -> Env -> Expr -> FVal Source #

Makes constant function if name is empty.

isFun :: Val -> Bool Source #

Is a value a function? May become more True after forcing the VUp.

absName :: FVal -> Name Source #

type FVal = Val Source #

type TVal = Val Source #

type Clos = Val Source #

type Domain = Dom TVal Source #

newtype Valuation Source #

Valuation of free variables.

Constructors

Valuation
Fields valuation :: [(Int, Val)]

Instances

Instances details

Reval Valuation Source #	When combining valuations, the old one takes priority. `[sigma][tau]v = [[sigma]tau]v`
Instance details Defined in Eval Methods reval' :: Valuation -> Valuation -> TypeCheck Valuation Source # reval :: Valuation -> TypeCheck Valuation Source #
Substitute Substitution Source #
Instance details Defined in TypeChecker Methods substitute :: Substitution -> Substitution -> TypeCheck Substitution Source #
Eq Valuation Source #
Instance details Defined in Value Methods (==) :: Valuation -> Valuation -> Bool # (/=) :: Valuation -> Valuation -> Bool #
Ord Valuation Source #
Instance details Defined in Value Methods compare :: Valuation -> Valuation -> Ordering # (<) :: Valuation -> Valuation -> Bool # (<=) :: Valuation -> Valuation -> Bool # (>) :: Valuation -> Valuation -> Bool # (>=) :: Valuation -> Valuation -> Bool # max :: Valuation -> Valuation -> Valuation # min :: Valuation -> Valuation -> Valuation #

emptyVal :: Valuation Source #

sgVal :: Int -> Val -> Valuation Source #

valuateGen :: Int -> Valuation -> Val Source #

type TeleVal = [TBinding Val] Source #

data Environ a Source #

Constructors

Environ
Fields envMap :: [(Name, a)] envBound :: Maybe (Measure Val)

Instances

Instances details

Reval Env Source #
Instance details Defined in Eval Methods reval' :: Valuation -> Env -> TypeCheck Env Source # reval :: Env -> TypeCheck Env Source #
Substitute Env Source #	Substitute in environment.
Instance details Defined in TypeChecker Methods substitute :: Substitution -> Env -> TypeCheck Env Source #
Show a => Show (Environ a) Source #
Instance details Defined in Value Methods showsPrec :: Int -> Environ a -> ShowS # show :: Environ a -> String # showList :: [Environ a] -> ShowS #
Eq a => Eq (Environ a) Source #
Instance details Defined in Value Methods (==) :: Environ a -> Environ a -> Bool # (/=) :: Environ a -> Environ a -> Bool #
Ord a => Ord (Environ a) Source #
Instance details Defined in Value Methods compare :: Environ a -> Environ a -> Ordering # (<) :: Environ a -> Environ a -> Bool # (<=) :: Environ a -> Environ a -> Bool # (>) :: Environ a -> Environ a -> Bool # (>=) :: Environ a -> Environ a -> Bool # max :: Environ a -> Environ a -> Environ a # min :: Environ a -> Environ a -> Environ a #