Core.TT

Contents

• A few handy operations on well typed terms:

Description

Synopsis

• data Option
  • = TTypeInTType
  • | CheckConv
• data FC = FC {
  • fc_fname :: String
  • fc_line :: Int
  • fc_column :: Int
  }
• newtype FC' = FC' {
  • unwrapFC :: FC
  }
• emptyFC :: FC
• fileFC :: String -> FC
• data Err
  • = Msg String
  • | InternalMsg String
  • | CantUnify Bool Term Term Err [(Name, Type)] Int
  • | InfiniteUnify Name Term [(Name, Type)]
  • | CantConvert Term Term [(Name, Type)]
  • | UnifyScope Name Name Term [(Name, Type)]
  • | CantInferType String
  • | NonFunctionType Term Term
  • | CantIntroduce Term
  • | NoSuchVariable Name
  • | NoTypeDecl Name
  • | NotInjective Term Term Term
  • | CantResolve Term
  • | CantResolveAlts [String]
  • | IncompleteTerm Term
  • | UniverseError
  • | ProgramLineComment
  • | Inaccessible Name
  • | NonCollapsiblePostulate Name
  • | AlreadyDefined Name
  • | ProofSearchFail Err
  • | NoRewriting Term
  • | At FC Err
  • | Elaborating String Name Err
  • | ProviderError String
  • | LoadingFailed String Err
• score :: Err -> Int
• data TC a
  • = OK a
  • | Error Err
• tfail :: Err -> TC a
• trun :: FC -> TC a -> TC a
• discard :: Monad m => m a -> m ()
• showSep :: String -> [String] -> String
• pmap :: (t -> t1) -> (t, t) -> (t1, t1)
• traceWhen :: Bool -> String -> a -> a
• data Name
  • = UN String
  • | NS Name [String]
  • | MN Int String
  • | NErased
  • | SN SpecialName
• data SpecialName
  • = WhereN Int Name Name
  • | InstanceN Name [String]
  • | ParentN Name String
  • | MethodN Name
  • | CaseN Name
• showCG :: Name -> String
• type Ctxt a = Map Name (Map Name a)
• emptyContext :: Map k a
• tcname :: Name -> Bool
• implicitable :: Name -> Bool
• nsroot :: Name -> Name
• addDef :: Name -> a -> Ctxt a -> Ctxt a
• lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
• lookupCtxt :: Name -> Ctxt a -> [a]
• lookupCtxtExact :: Name -> Ctxt a -> [a]
• updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
• toAlist :: Ctxt a -> [(Name, a)]
• addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a
• data NativeTy
  • = IT8
  • | IT16
  • | IT32
  • | IT64
• data IntTy
  • = ITFixed NativeTy
  • | ITNative
  • | ITBig
  • | ITChar
  • | ITVec NativeTy Int
• data ArithTy
  • = ATInt IntTy
  • | ATFloat
• nativeTyWidth :: NativeTy -> Int
• intTyWidth :: IntTy -> Int
• data Const
  • = I Int
  • | BI Integer
  • | Fl Double
  • | Ch Char
  • | Str String
  • | B8 Word8
  • | B16 Word16
  • | B32 Word32
  • | B64 Word64
  • | B8V (Vector Word8)
  • | B16V (Vector Word16)
  • | B32V (Vector Word32)
  • | B64V (Vector Word64)
  • | AType ArithTy
  • | StrType
  • | PtrType
  • | VoidType
  • | Forgot
• data Raw
  • = Var Name
  • | RBind Name (Binder Raw) Raw
  • | RApp Raw Raw
  • | RType
  • | RForce Raw
  • | RConstant Const
• data Binder b
  • = Lam {
    • binderTy :: b
    }
  • | Pi {
    • binderTy :: b
    }
  • | Let {
    • binderTy :: b
    • binderVal :: b
    }
  • | NLet {
    • binderTy :: b
    • binderVal :: b
    }
  • | Hole {
    • binderTy :: b
    }
  • | GHole {
    • envlen :: Int
    • binderTy :: b
    }
  • | Guess {
    • binderTy :: b
    • binderVal :: b
    }
  • | PVar {
    • binderTy :: b
    }
  • | PVTy {
    • binderTy :: b
    }
• fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
• raw_apply :: Raw -> [Raw] -> Raw
• raw_unapply :: Raw -> (Raw, [Raw])
• data RawFun = RawFun {
  • rtype :: Raw
  • rval :: Raw
  }
• data RawDatatype = RDatatype Name Raw [(Name, Raw)]
• data RDef
  • = RFunction RawFun
  • | RConst Raw
  • | RData RawDatatype
• type RProgram = [(Name, RDef)]
• data UExp
  • = UVar Int
  • | UVal Int
• data UConstraint
  • = ULT UExp UExp
  • | ULE UExp UExp
• type UCs = (Int, [UConstraint])
• data NameType
  • = Bound
  • | Ref
  • | DCon Int Int
  • | TCon Int Int
• data TT n
  • = P NameType n (TT n)
  • | V Int
  • | Bind n (Binder (TT n)) (TT n)
  • | App (TT n) (TT n)
  • | Constant Const
  • | Proj (TT n) Int
  • | Erased
  • | Impossible
  • | TType UExp
• class TermSize a where
  • termsize :: Name -> a -> Int
• type EnvTT n = [(n, Binder (TT n))]
• data Datatype n = Data {
  • d_typename :: n
  • d_typetag :: Int
  • d_type :: TT n
  • d_cons :: [(n, TT n)]
  }
• isInjective :: TT n -> Bool
• vinstances :: Int -> TT n -> Int
• instantiate :: TT n -> TT n -> TT n
• substV :: TT n -> TT n -> TT n
• explicitNames :: TT n -> TT n
• pToV :: Eq n => n -> TT n -> TT n
• pToV' :: Eq n => n -> Int -> TT n -> TT n
• addBinder :: TT n -> TT n
• pToVs :: Eq n => [n] -> TT n -> TT n
• vToP :: TT n -> TT n
• finalise :: Eq n => TT n -> TT n
• subst :: Eq n => n -> TT n -> TT n -> TT n
• substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
• substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
• noOccurrence :: Eq n => n -> TT n -> Bool
• freeNames :: Eq n => TT n -> [n]
• arity :: TT n -> Int
• unApply :: TT n -> (TT n, [TT n])
• mkApp :: TT n -> [TT n] -> TT n
• forget :: TT Name -> Raw
• bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
• bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
• getArgTys :: TT n -> [(n, TT n)]
• getRetTy :: TT n -> TT n
• uniqueName :: Name -> [Name] -> Name
• uniqueBinders :: [Name] -> TT Name -> TT Name
• nextName :: Name -> Name
• type Term = TT Name
• type Type = Term
• type Env = EnvTT Name
• newtype WkEnvTT n = Wk (EnvTT n)
• type WkEnv = WkEnvTT Name
• itBitsName :: NativeTy -> [Char]
• showEnv :: (Eq a, Show a) => [(a, Binder (TT a))] -> TT a -> [Char]
• showEnvDbg :: (Eq a, Show a) => [(a, Binder (TT a))] -> TT a -> [Char]
• prettyEnv :: (Eq a, Show a, Pretty a) => [(a, Binder (TT a))] -> TT a -> Doc
• showEnv' :: (Eq a, Show a) => [(a, Binder (TT a))] -> TT a -> Bool -> [Char]
• pureTerm :: TT Name -> Bool
• weakenTm :: Int -> TT n -> TT n
• weakenEnv :: EnvTT n -> EnvTT n
• weakenTmEnv :: Int -> EnvTT n -> EnvTT n
• orderPats :: Term -> Term

Documentation

A few handy operations on well typed terms: