mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 16:51:51 +03:00
e1dbcad2fc
Don't get too excited yet - I want this in so that it doesn't get too out of sync, but I still have to think about exactly how it's going to work in practice.
83 lines
2.0 KiB
Idris
83 lines
2.0 KiB
Idris
module Language.Reflection.TT
|
|
|
|
public export
|
|
FilePos : Type
|
|
FilePos = (Int, Int)
|
|
|
|
public export
|
|
data FC : Type where
|
|
MkFC : String -> FilePos -> FilePos -> FC
|
|
EmptyFC : FC
|
|
|
|
public export
|
|
emptyFC : FC
|
|
emptyFC = EmptyFC
|
|
|
|
public export
|
|
data NameType : Type where
|
|
Bound : NameType
|
|
Func : NameType
|
|
DataCon : (tag : Int) -> (arity : Nat) -> NameType
|
|
TyCon : (tag : Int) -> (arity : Nat) -> NameType
|
|
|
|
public export
|
|
data Constant
|
|
= I Int
|
|
| BI Integer
|
|
| Str String
|
|
| Ch Char
|
|
| Db Double
|
|
| WorldVal
|
|
|
|
| IntType
|
|
| IntegerType
|
|
| StringType
|
|
| CharType
|
|
| DoubleType
|
|
| WorldType
|
|
|
|
public export
|
|
data Name = UN String
|
|
| MN String Int
|
|
| NS (List String) Name
|
|
|
|
public export
|
|
data Count = M0 | M1 | MW
|
|
|
|
public export
|
|
data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t
|
|
|
|
public export
|
|
data IsVar : Name -> Nat -> List Name -> Type where
|
|
First : IsVar n Z (n :: ns)
|
|
Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
|
|
|
|
public export
|
|
data LazyReason = LInf | LLazy | LUnknown
|
|
|
|
-- Type checked terms in the core TT
|
|
public export
|
|
data TT : List Name -> Type where
|
|
Local : FC -> (idx : Nat) -> (0 prf : IsVar name idx vars) -> TT vars
|
|
Ref : FC -> NameType -> Name -> TT vars
|
|
Pi : FC -> Count -> PiInfo (TT vars) ->
|
|
(x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
|
|
TT vars
|
|
Lam : FC -> Count -> PiInfo (TT vars) ->
|
|
(x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
|
|
TT vars
|
|
App : FC -> TT vars -> TT vars -> TT vars
|
|
TDelayed : FC -> LazyReason -> TT vars -> TT vars
|
|
TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
|
|
TForce : FC -> LazyReason -> TT vars -> TT vars
|
|
PrimVal : FC -> Constant -> TT vars
|
|
Erased : FC -> TT vars
|
|
TType : FC -> TT vars
|
|
|
|
public export
|
|
data TotalReq = Total | CoveringOnly | PartialOK
|
|
|
|
public export
|
|
data Visibility = Private | Export | Public
|
|
|