Language.Symantic.Compiling.Read

Type ReadTerm

type ReadTerm src ss ts = Source src => SourceInj (TypeVT src) src => SourceInj (KindK src) src => SourceInj (AST_Type src) src => Constable (->) => CtxTy src ts -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss ts)

Convenient type alias for readTerm and related functions.

readTerm :: forall src ss ts. ReadTerm src ss ts

Read a TermVT from and AST_Term.

teVar :: forall ss src ts. Source src => NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)

teApp :: Source src => Constable (->) => Term src ss ts '[Proxy (a :: Type), Proxy (b :: Type)] (() #> ((a -> b) -> a -> b))

reduceTeApp :: AST_Term src ss -> AST_Term src ss

Reduce number of Token_Term_App in given AST_Term by converting them into BinTree2.

NOTE: Token_Term_App exists only to handle unifix operators applied to arguments.

Type ReadTermCF

newtype ReadTermCF src ss

Like ReadTerm, but CtxTe-free.

Useful in readTermWithCtx to help GHC's type solver, which "Cannot instantiate unification variable with a type involving foralls".

Constructors

ReadTermCF

Fields

• unReadTermCF :: forall ts. ReadTerm src ss ts

readTermWithCtx :: Foldable f => Source src => SourceInj (TypeVT src) src => SourceInj (KindK src) src => SourceInj (AST_Type src) src => Constable (->) => f (NameTe, TermT src ss '[] '[]) -> AST_Term src ss -> Either (Error_Term src) (TermVT src ss '[])

Like readTerm but with given context, and no more.

readTermWithCtxPush :: Foldable f => f (NameTe, TermT src ss '[] '[]) -> (forall ts'. ReadTerm src ss ts') -> ReadTerm src ss ts

Like readTerm but with given context.

readTermWithCtxPush1 :: (NameTe, TermT src ss '[] '[]) -> (forall ts'. ReadTerm src ss ts') -> ReadTerm src ss ts

Like readTerm but with given TermT pushed onto CtxTy and CtxTe.

readTermWithCtxClose :: (forall ts'. ReadTerm src ss ts') -> Source src => SourceInj (TypeVT src) src => SourceInj (KindK src) src => SourceInj (AST_Type src) src => Constable (->) => AST_Term src ss -> Either (Error_Term src) (TermVT src ss '[])

Close a ReadTerm context.

Type CtxTy

data CtxTy src ts where

Typing context accumulating at each lambda abstraction the Type of the introduced variable. It is built top-down from the closest including lambda abstraction to the farest. It determines the Types of CtxTe.

Constructors

CtxTyZ :: CtxTy src '[]

CtxTyS :: NameTe -> Type src '[] t -> CtxTy src ts -> CtxTy src (t ': ts) infixr 5

appendCtxTy :: CtxTy src ts0 -> CtxTy src ts1 -> CtxTy src (ts0 ++ ts1)

Type Error_Term

data Error_Term src

Constructors

Error_Term_unknown NameTe

Error_Term_polymorphic (TypeVT src)

Error_Term_qualified (TypeVT src)

Error_Term_proofless (TypeVT src)

Error_Term_Type (Error_Type src)

Error_Term_Beta (Error_Beta src)

Instances

(Eq src, Source src) => Eq (Error_Term src)

Methods

(==) :: Error_Term src -> Error_Term src -> Bool

(/=) :: Error_Term src -> Error_Term src -> Bool

(Show src, Source src) => Show (Error_Term src)

Methods

showsPrec :: Int -> Error_Term src -> ShowS

show :: Error_Term src -> String

showList :: [Error_Term src] -> ShowS

ErrorInj (Con_Kind src) (Error_Term src)

Methods

errorInj :: Con_Kind src -> Error_Term src

ErrorInj (Error_Type src) (Error_Term src)

Methods

errorInj :: Error_Type src -> Error_Term src

ErrorInj (Error_Beta src) (Error_Term src)

Methods

errorInj :: Error_Beta src -> Error_Term src

Type SrcTe

data SrcTe inp ss

A Source usable when using readTerm.

Constructors

SrcTe_Less

SrcTe_Input (Span inp)

SrcTe_AST_Term (AST_Term (SrcTe inp ss) ss)

SrcTe_AST_Type (AST_Type (SrcTe inp ss))

SrcTe_Kind (KindK (SrcTe inp ss))

SrcTe_Type (TypeVT (SrcTe inp ss))

SrcTe_Term

Instances

SourceInj (Span inp) (SrcTe inp ss)

Methods

sourceInj :: Span inp -> SrcTe inp ss

SourceInj (KindK (SrcTe inp ss)) (SrcTe inp ss)

Methods

sourceInj :: KindK (SrcTe inp ss) -> SrcTe inp ss

SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss)

Methods

sourceInj :: TypeVT (SrcTe inp ss) -> SrcTe inp ss

SourceInj (AST_Type (SrcTe inp ss)) (SrcTe inp ss)

Methods

sourceInj :: AST_Type (SrcTe inp ss) -> SrcTe inp ss

Eq inp => Eq (SrcTe inp ss)

Methods

(==) :: SrcTe inp ss -> SrcTe inp ss -> Bool

(/=) :: SrcTe inp ss -> SrcTe inp ss -> Bool

Show inp => Show (SrcTe inp ss)

Methods

showsPrec :: Int -> SrcTe inp ss -> ShowS

show :: SrcTe inp ss -> String

showList :: [SrcTe inp ss] -> ShowS

Source (SrcTe inp ss)

Methods

noSource :: SrcTe inp ss

SourceInj (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss)

Methods

sourceInj :: AST_Term (SrcTe inp ss) ss -> SrcTe inp ss

type Source_Input (SrcTe inp ss)

type Source_Input (SrcTe inp ss) = inp