MiniAgda
Safe HaskellNone
LanguageHaskell98

Eval

Synopsis

Documentation

traceEta :: String -> a -> a Source #

traceEtaM :: Monad m => String -> m () Source #

traceRecord :: String -> a -> a Source #

traceRecordM :: Monad m => String -> m () Source #

traceMatch :: String -> a -> a Source #

traceMatchM :: Monad m => String -> m () Source #

traceLoop :: String -> a -> a Source #

traceLoopM :: Monad m => String -> m () Source #

traceSize :: String -> a -> a Source #

traceSizeM :: Monad m => String -> m () Source #

failValInv :: MonadError TraceError m => Val -> m a Source #

class Reval a where Source #

Minimal complete definition

reval'

Methods

reval' :: Valuation -> a -> TypeCheck a Source #

reval :: a -> TypeCheck a Source #

Instances

Instances details
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 #

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 #

Reval a => Reval (Bound a) Source # 
Instance details

Defined in Eval

Methods

reval' :: Valuation -> Bound a -> TypeCheck (Bound a) Source #

reval :: Bound a -> TypeCheck (Bound a) Source #

Reval a => Reval (Measure a) Source # 
Instance details

Defined in Eval

Methods

reval' :: Valuation -> Measure a -> TypeCheck (Measure a) Source #

reval :: Measure a -> TypeCheck (Measure a) Source #

Reval a => Reval (Maybe a) Source # 
Instance details

Defined in Eval

Methods

reval' :: Valuation -> Maybe a -> TypeCheck (Maybe a) Source #

reval :: Maybe a -> TypeCheck (Maybe a) Source #

Reval a => Reval [a] Source # 
Instance details

Defined in Eval

Methods

reval' :: Valuation -> [a] -> TypeCheck [a] Source #

reval :: [a] -> TypeCheck [a] Source #

Reval b => Reval (a, b) Source # 
Instance details

Defined in Eval

Methods

reval' :: Valuation -> (a, b) -> TypeCheck (a, b) Source #

reval :: (a, b) -> TypeCheck (a, b) Source #

vSing :: Val -> TVal -> TypeCheck TVal Source #

reduce :: Val -> TypeCheck Val Source #

equal :: Val -> Val -> TypeCheck Bool Source #

notDifferentNames :: RecInfo -> RecInfo -> Bool Source #

equals' :: [Val] -> [Val] -> TypeCheck Bool Source #

equal' :: Val -> Val -> TypeCheck Bool Source #

reify :: Val -> TypeCheck Expr Source #

reify' :: (Int, Bool) -> Val -> TypeCheck Expr Source #

toExpr :: Val -> TypeCheck Expr Source #

addNameEnv :: Name -> Env -> (Name -> Env -> TypeCheck a) -> TypeCheck a Source #

addPatternEnv :: Pattern -> Env -> (Pattern -> Env -> TypeCheck a) -> TypeCheck a Source #

addPatternsEnv :: [Pattern] -> Env -> ([Pattern] -> Env -> TypeCheck a) -> TypeCheck a Source #

class ClosToExpr a where Source #

Minimal complete definition

Nothing

Methods

closToExpr :: Env -> a -> TypeCheck a Source #

bindClosToExpr :: Env -> a -> (Env -> a -> TypeCheck b) -> TypeCheck b Source #

Instances

Instances details
ClosToExpr Expr Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Expr -> TypeCheck Expr Source #

bindClosToExpr :: Env -> Expr -> (Env -> Expr -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr Telescope Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Telescope -> TypeCheck Telescope Source #

bindClosToExpr :: Env -> Telescope -> (Env -> Telescope -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (Bound a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Bound a -> TypeCheck (Bound a) Source #

bindClosToExpr :: Env -> Bound a -> (Env -> Bound a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (Dom a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Dom a -> TypeCheck (Dom a) Source #

bindClosToExpr :: Env -> Dom a -> (Env -> Dom a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (Measure a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Measure a -> TypeCheck (Measure a) Source #

bindClosToExpr :: Env -> Measure a -> (Env -> Measure a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (Sort a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Sort a -> TypeCheck (Sort a) Source #

bindClosToExpr :: Env -> Sort a -> (Env -> Sort a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (TBinding a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> TBinding a -> TypeCheck (TBinding a) Source #

bindClosToExpr :: Env -> TBinding a -> (Env -> TBinding a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (Tagged a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Tagged a -> TypeCheck (Tagged a) Source #

bindClosToExpr :: Env -> Tagged a -> (Env -> Tagged a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr (Maybe a) Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> Maybe a -> TypeCheck (Maybe a) Source #

bindClosToExpr :: Env -> Maybe a -> (Env -> Maybe a -> TypeCheck b) -> TypeCheck b Source #

ClosToExpr a => ClosToExpr [a] Source # 
Instance details

Defined in Eval

Methods

closToExpr :: Env -> [a] -> TypeCheck [a] Source #

bindClosToExpr :: Env -> [a] -> (Env -> [a] -> TypeCheck b) -> TypeCheck b Source #

metaToExpr :: Int -> Env -> Int -> TypeCheck Expr Source #

clauseToExpr :: Env -> Clause -> TypeCheck Clause Source #

whnf :: Env -> Expr -> TypeCheck Val Source #

Weak head normal form. Monadic, since it reads the globally defined constants from the signature. lets are expanded away.

whnfMeasure :: Env -> Measure Expr -> TypeCheck (Measure Val) Source #

whnfSort :: Env -> Sort Expr -> TypeCheck (Sort Val) Source #

whnfClos :: Clos -> TypeCheck Val Source #

whnf' :: Expr -> TypeCheck Val Source #

sing :: Env -> Expr -> TVal -> TypeCheck TVal Source #

sing' :: Expr -> TVal -> TypeCheck TVal Source #

evalCase :: Val -> TVal -> Env -> [Clause] -> TypeCheck Val Source #

piApp :: TVal -> Clos -> TypeCheck TVal Source #

piApps :: TVal -> [Clos] -> TypeCheck TVal Source #

updateValu :: Valuation -> Int -> Val -> TypeCheck Valuation Source #

app :: Val -> Clos -> TypeCheck Val Source #

app' :: Bool -> Val -> Clos -> TypeCheck Val Source #

Application of arguments and projections.

force' :: Bool -> Val -> TypeCheck (Bool, Val) Source #

force :: Val -> TypeCheck Val Source #

appDef :: QName -> [Val] -> TypeCheck Val Source #

up :: Bool -> Val -> TVal -> TypeCheck Val Source #

matchingConstructors :: Val -> TypeCheck (Maybe [(ConstructorInfo, Env)]) Source #

matchingConstructors' :: QName -> [Val] -> TypeCheck [(ConstructorInfo, Env)] Source #

matchingConstructors'' :: Bool -> [Val] -> Val -> [ConstructorInfo] -> TypeCheck [(ConstructorInfo, Env)] Source #

data MatchingConstructors a Source #

Constructors

NoConstructor 
OneConstructor a 
ManyConstructors 
UnknownConstructors 

Instances

Instances details
Show a => Show (MatchingConstructors a) Source # 
Instance details

Defined in Eval

Methods

showsPrec :: Int -> MatchingConstructors a -> ShowS #

show :: MatchingConstructors a -> String #

showList :: [MatchingConstructors a] -> ShowS #

Eq a => Eq (MatchingConstructors a) Source # 
Instance details

Defined in Eval

Methods

(==) :: MatchingConstructors a -> MatchingConstructors a -> Bool #

(/=) :: MatchingConstructors a -> MatchingConstructors a -> Bool #

getMatchingConstructor :: Bool -> QName -> [Val] -> TypeCheck (MatchingConstructors (Co, [Val], Env, [Val], ConstructorInfo)) Source #

getFieldsAtType :: QName -> [Val] -> TypeCheck (Maybe [(Name, TVal)]) Source #

projectType :: TVal -> Name -> Val -> TypeCheck TVal Source #

upData :: Bool -> Val -> QName -> [Val] -> TypeCheck Val Source #

matchClauses :: Env -> [Clause] -> [Val] -> TypeCheck (Maybe Val) Source #

bindMaybe :: Monad m => m (Maybe a) -> (a -> m (Maybe b)) -> m (Maybe b) Source #

matchClause :: Env -> [Pattern] -> Expr -> [Val] -> TypeCheck (Maybe Val) Source #

match :: Env -> Pattern -> Val -> TypeCheck (Maybe Env) Source #

matchList :: Env -> [Pattern] -> [Val] -> TypeCheck (Maybe Env) Source #

Typed Non-linear Matching -----------------------------------------

type GenToPattern = [(Int, Pattern)] Source #

type MatchState = (Env, GenToPattern) Source #

nonLinMatch :: Bool -> Bool -> MatchState -> Pattern -> Val -> TVal -> TypeCheck (Maybe MatchState) Source #

nonLinMatchList :: Bool -> Env -> [Pattern] -> [Val] -> TVal -> TypeCheck (Maybe Env) Source #

nonLinMatchList' :: Bool -> Bool -> MatchState -> [Pattern] -> [Val] -> TVal -> TypeCheck (Maybe MatchState) Source #

expandDefPat :: Pattern -> TypeCheck Pattern Source #

Expand a top-level pattern synonym

Unification

class Nocc a where Source #

Occurrence check nocc ks v (used by SPos and TypeCheck). Checks that generic values ks does not occur in value v. In the process, tv is normalized.

Methods

nocc :: [Int] -> a -> TypeCheck Bool Source #

Instances

Instances details
Nocc Val Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> Val -> TypeCheck Bool Source #

Nocc a => Nocc (Bound a) Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> Bound a -> TypeCheck Bool Source #

Nocc a => Nocc (Dom a) Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> Dom a -> TypeCheck Bool Source #

Nocc a => Nocc (Measure a) Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> Measure a -> TypeCheck Bool Source #

Nocc a => Nocc (Sort a) Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> Sort a -> TypeCheck Bool Source #

Nocc a => Nocc [a] Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> [a] -> TypeCheck Bool Source #

(Nocc a, Nocc b) => Nocc (a, b) Source # 
Instance details

Defined in Eval

Methods

nocc :: [Int] -> (a, b) -> TypeCheck Bool Source #

eqValBool :: TVal -> Val -> Val -> TypeCheck Bool Source #

eqVal :: TVal -> Val -> Val -> TypeCheck () Source #

data Force Source #

Constructors

N 
L 
R 

Instances

Instances details
Switchable Force Source # 
Instance details

Defined in Eval

Methods

switch :: Force -> Force Source #

Show Force Source # 
Instance details

Defined in Eval

Methods

showsPrec :: Int -> Force -> ShowS #

show :: Force -> String #

showList :: [Force] -> ShowS #

Eq Force Source # 
Instance details

Defined in Eval

Methods

(==) :: Force -> Force -> Bool #

(/=) :: Force -> Force -> Bool #

class Switchable a where Source #

Methods

switch :: a -> a Source #

Instances

Instances details
Switchable Force Source # 
Instance details

Defined in Eval

Methods

switch :: Force -> Force Source #

Switchable Pol Source # 
Instance details

Defined in Eval

Methods

switch :: Pol -> Pol Source #

Switchable a => Switchable (Maybe a) Source # 
Instance details

Defined in Eval

Methods

switch :: Maybe a -> Maybe a Source #

Switchable (a, a) Source # 
Instance details

Defined in Eval

Methods

switch :: (a, a) -> (a, a) Source #

leqDec :: Pol -> Dec -> Dec -> Bool Source #

subtype :: Val -> Val -> TypeCheck () Source #

leqVal :: Pol -> TVal -> Val -> Val -> TypeCheck () Source #

type MT12 = Maybe (OneOrTwo TVal) Source #

data TypeShape Source #

Constructors

ShQuant PiSigma (OneOrTwo Name) (OneOrTwo Domain) (OneOrTwo FVal) 
ShSort SortShape 
ShData QName (OneOrTwo TVal) 
ShNe (OneOrTwo TVal) 
ShSing Val TVal 
ShSingL Val TVal TVal 
ShSingR TVal Val TVal 
ShNone 

Instances

Instances details
Eq TypeShape Source # 
Instance details

Defined in Eval

Methods

(==) :: TypeShape -> TypeShape -> Bool #

(/=) :: TypeShape -> TypeShape -> Bool #

Ord TypeShape Source # 
Instance details

Defined in Eval

Methods

compare :: TypeShape -> TypeShape -> Ordering #

(<) :: TypeShape -> TypeShape -> Bool #

(<=) :: TypeShape -> TypeShape -> Bool #

(>) :: TypeShape -> TypeShape -> Bool #

(>=) :: TypeShape -> TypeShape -> Bool #

max :: TypeShape -> TypeShape -> TypeShape #

min :: TypeShape -> TypeShape -> TypeShape #

data SortShape Source #

Constructors

ShSortC Class 
ShSet (OneOrTwo Val) 
ShCoSet (OneOrTwo Val) 

Instances

Instances details
Eq SortShape Source # 
Instance details

Defined in Eval

Methods

(==) :: SortShape -> SortShape -> Bool #

(/=) :: SortShape -> SortShape -> Bool #

Ord SortShape Source # 
Instance details

Defined in Eval

Methods

compare :: SortShape -> SortShape -> Ordering #

(<) :: SortShape -> SortShape -> Bool #

(<=) :: SortShape -> SortShape -> Bool #

(>) :: SortShape -> SortShape -> Bool #

(>=) :: SortShape -> SortShape -> Bool #

max :: SortShape -> SortShape -> SortShape #

min :: SortShape -> SortShape -> SortShape #

shSize :: TypeShape Source #

typeView :: TVal -> TypeShape Source #

sortView :: Sort Val -> SortShape Source #

typeView12 :: (Functor m, Monad m, MonadError TraceError m) => OneOrTwo TVal -> m TypeShape Source #

sortView12 :: (Monad m, MonadError TraceError m) => OneOrTwo (Sort Val) -> m SortShape Source #

whnf12 :: OneOrTwo Env -> OneOrTwo Expr -> TypeCheck (OneOrTwo Val) Source #

app12 :: OneOrTwo Val -> OneOrTwo Val -> TypeCheck (OneOrTwo Val) Source #

leqVal' :: Force -> Pol -> MT12 -> Val -> Val -> TypeCheck () Source #

leqClauses :: Force -> Pol -> MT12 -> Val -> TVal -> Env -> [Clause] -> Env -> [Clause] -> TypeCheck () Source #

type NameMap = [(Name, Name)] Source #

alphaPattern :: Pattern -> Pattern -> StateT NameMap TypeCheck () Source #

leqCases :: Force -> Pol -> MT12 -> Val -> Val -> TVal -> Env -> [Clause] -> TypeCheck () Source #

leqCase :: Force -> Pol -> MT12 -> Val -> Val -> TVal -> Env -> Clause -> TypeCheck () Source #

leqVals' :: Force -> Pol -> OneOrTwo TVal -> [Val] -> [Val] -> TypeCheck (OneOrTwo TVal) Source #

leqApp :: Force -> Pol -> Val -> [Val] -> Val -> [Val] -> TypeCheck () Source #

isEmptyType :: TVal -> TypeCheck Bool Source #

isUnitType :: TVal -> TypeCheck Bool Source #

leqSort :: Pol -> Sort Val -> Sort Val -> TypeCheck () Source #

leqSort' :: Sort Val -> Sort Val -> TypeCheck () Source #

minSize :: Val -> Val -> Maybe Val Source #

maxMins :: [Maybe Val] -> Maybe Val Source #

leqSize :: Pol -> Val -> Val -> TypeCheck () Source #

ltSize :: Val -> Val -> TypeCheck () Source #

leSize :: LtLe -> Pol -> Val -> Val -> TypeCheck () Source #

leqSize' :: Val -> Val -> TypeCheck () Source #

leSize' :: LtLe -> Val -> Val -> TypeCheck () Source #

leSize'' :: LtLe -> Int -> Val -> Val -> TypeCheck () Source #

leSizePlus :: LtLe -> Int -> [Val] -> [Val] -> TypeCheck () Source #

varBelowInfty :: Val -> TypeCheck Bool Source #

leSizePlus' :: LtLe -> Int -> [Val] -> [Val] -> TypeCheck () Source #

tryIrregularBound :: Int -> Int -> Int -> TypeCheck () Source #

lexSizes :: LtLe -> [Val] -> [Val] -> TypeCheck () Source #

entailsGuard :: Pol -> Bound Val -> Bound Val -> TypeCheck () Source #

checkGuard :: Bound Val -> TypeCheck () Source #

addOrCheckGuard :: Pol -> Bound Val -> TypeCheck a -> TypeCheck a Source #

leqPolM :: Pol -> PProd -> TypeCheck () Source #

leqPolPoly :: Pol -> PPoly -> TypeCheck () Source #

addPosEdge :: DefId -> DefId -> PProd -> TypeCheck () Source #

checkPositivityGraph :: TypeCheck () Source #

telView :: TVal -> TypeCheck ([(Val, TBinding TVal)], TVal) Source #

mkConVal :: Dotted -> ConK -> QName -> [Val] -> TVal -> TypeCheck Val Source #

Turn a fully applied constructor value into a named record value.

Orphan instances